Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lvolnle3at Structured version   Visualization version   GIF version

Theorem lvolnle3at 35406
Description: A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.)
Hypotheses
Ref Expression
lvolnle3at.l = (le‘𝐾)
lvolnle3at.j = (join‘𝐾)
lvolnle3at.a 𝐴 = (Atoms‘𝐾)
lvolnle3at.v 𝑉 = (LVols‘𝐾)
Assertion
Ref Expression
lvolnle3at (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))

Proof of Theorem lvolnle3at
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simplr 774 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → 𝑋𝑉)
2 eqid 2774 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
3 eqid 2774 . . . . . 6 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4 eqid 2774 . . . . . 6 (LPlanes‘𝐾) = (LPlanes‘𝐾)
5 lvolnle3at.v . . . . . 6 𝑉 = (LVols‘𝐾)
62, 3, 4, 5islvol 35397 . . . . 5 (𝐾 ∈ HL → (𝑋𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
76ad2antrr 706 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑋𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
81, 7mpbid 223 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
98simprd 484 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10 oveq1 6819 . . . . . . . . 9 (𝑃 = 𝑄 → (𝑃 𝑄) = (𝑄 𝑄))
1110oveq1d 6827 . . . . . . . 8 (𝑃 = 𝑄 → ((𝑃 𝑄) 𝑅) = ((𝑄 𝑄) 𝑅))
1211breq2d 4809 . . . . . . 7 (𝑃 = 𝑄 → (𝑋 ((𝑃 𝑄) 𝑅) ↔ 𝑋 ((𝑄 𝑄) 𝑅)))
1312notbid 308 . . . . . 6 (𝑃 = 𝑄 → (¬ 𝑋 ((𝑃 𝑄) 𝑅) ↔ ¬ 𝑋 ((𝑄 𝑄) 𝑅)))
14 simp1l 1245 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
15 simp3l 1249 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LPlanes‘𝐾))
16 simp21 1254 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑃𝐴)
17 simp22 1255 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑄𝐴)
18 lvolnle3at.l . . . . . . . . . . . . 13 = (le‘𝐾)
19 lvolnle3at.j . . . . . . . . . . . . 13 = (join‘𝐾)
20 lvolnle3at.a . . . . . . . . . . . . 13 𝐴 = (Atoms‘𝐾)
2118, 19, 20, 4lplnnle2at 35365 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑃𝐴𝑄𝐴)) → ¬ 𝑦 (𝑃 𝑄))
2214, 15, 16, 17, 21syl13anc 1481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 (𝑃 𝑄))
232, 4lplnbase 35358 . . . . . . . . . . . . . . 15 (𝑦 ∈ (LPlanes‘𝐾) → 𝑦 ∈ (Base‘𝐾))
2415, 23syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
25 simp1r 1246 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋𝑉)
262, 5lvolbase 35402 . . . . . . . . . . . . . . 15 (𝑋𝑉𝑋 ∈ (Base‘𝐾))
2725, 26syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
28 simp3r 1250 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
29 eqid 2774 . . . . . . . . . . . . . . 15 (lt‘𝐾) = (lt‘𝐾)
302, 29, 3cvrlt 35094 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
3114, 24, 27, 28, 30syl31anc 1482 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
32 hlpos 35190 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL → 𝐾 ∈ Poset)
3314, 32syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
342, 19, 20hlatjcl 35191 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
3514, 16, 17, 34syl3anc 1480 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑃 𝑄) ∈ (Base‘𝐾))
362, 18, 29pltletr 17199 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑃 𝑄)) → 𝑦(lt‘𝐾)(𝑃 𝑄)))
3733, 24, 27, 35, 36syl13anc 1481 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑃 𝑄)) → 𝑦(lt‘𝐾)(𝑃 𝑄)))
3831, 37mpand 676 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑃 𝑄) → 𝑦(lt‘𝐾)(𝑃 𝑄)))
3918, 29pltle 17189 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑃 𝑄) → 𝑦 (𝑃 𝑄)))
4014, 15, 35, 39syl3anc 1480 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑃 𝑄) → 𝑦 (𝑃 𝑄)))
4138, 40syld 47 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑃 𝑄) → 𝑦 (𝑃 𝑄)))
4222, 41mtod 189 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 (𝑃 𝑄))
4342adantr 467 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → ¬ 𝑋 (𝑃 𝑄))
44 simprr 778 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → 𝑅 (𝑃 𝑄))
4514hllatd 35188 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Lat)
46 simp23 1256 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅𝐴)
472, 20atbase 35113 . . . . . . . . . . . . . 14 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
4846, 47syl 17 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
492, 18, 19latleeqj2 17292 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
5045, 48, 35, 49syl3anc 1480 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
5150adantr 467 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
5244, 51mpbid 223 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑅) = (𝑃 𝑄))
5352breq2d 4809 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → (𝑋 ((𝑃 𝑄) 𝑅) ↔ 𝑋 (𝑃 𝑄)))
5443, 53mtbird 315 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
5554anassrs 454 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃𝑄) ∧ 𝑅 (𝑃 𝑄)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
56 simpl1l 1284 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → 𝐾 ∈ HL)
57 simpl3l 1292 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → 𝑦 ∈ (LPlanes‘𝐾))
58 simpl2 1235 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → (𝑃𝐴𝑄𝐴𝑅𝐴))
59 simpr 472 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄)))
6018, 19, 20, 4lplni2 35361 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑅) ∈ (LPlanes‘𝐾))
6156, 58, 59, 60syl3anc 1480 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑅) ∈ (LPlanes‘𝐾))
6229, 4lplnnlt 35389 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (LPlanes‘𝐾)) → ¬ 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅))
6356, 57, 61, 62syl3anc 1480 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ¬ 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅))
642, 19latjcl 17279 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
6545, 35, 48, 64syl3anc 1480 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
662, 18, 29pltletr 17199 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 ((𝑃 𝑄) 𝑅)) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
6733, 24, 27, 65, 66syl13anc 1481 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 ((𝑃 𝑄) 𝑅)) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
6831, 67mpand 676 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ((𝑃 𝑄) 𝑅) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
6968adantr 467 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → (𝑋 ((𝑃 𝑄) 𝑅) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
7063, 69mtod 189 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
7170anassrs 454 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃𝑄) ∧ ¬ 𝑅 (𝑃 𝑄)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
7255, 71pm2.61dan 836 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃𝑄) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
73 eqid 2774 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
7473, 19, 20, 4lplnnle2at 35365 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑄𝐴𝑅𝐴)) → ¬ 𝑦(le‘𝐾)(𝑄 𝑅))
7514, 15, 17, 46, 74syl13anc 1481 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦(le‘𝐾)(𝑄 𝑅))
762, 19, 20hlatjcl 35191 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
7714, 17, 46, 76syl3anc 1480 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 𝑅) ∈ (Base‘𝐾))
782, 18, 29pltletr 17199 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑄 𝑅)) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
7933, 24, 27, 77, 78syl13anc 1481 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑄 𝑅)) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
8031, 79mpand 676 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑄 𝑅) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
8173, 29pltle 17189 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑄 𝑅) → 𝑦(le‘𝐾)(𝑄 𝑅)))
8214, 15, 77, 81syl3anc 1480 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑄 𝑅) → 𝑦(le‘𝐾)(𝑄 𝑅)))
8380, 82syld 47 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑄 𝑅) → 𝑦(le‘𝐾)(𝑄 𝑅)))
8475, 83mtod 189 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 (𝑄 𝑅))
8519, 20hlatjidm 35193 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴) → (𝑄 𝑄) = 𝑄)
8614, 17, 85syl2anc 574 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 𝑄) = 𝑄)
8786oveq1d 6827 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑄 𝑄) 𝑅) = (𝑄 𝑅))
8887breq2d 4809 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ((𝑄 𝑄) 𝑅) ↔ 𝑋 (𝑄 𝑅)))
8984, 88mtbird 315 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ((𝑄 𝑄) 𝑅))
9013, 72, 89pm2.61ne 3031 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
91903expia 1141 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ((𝑃 𝑄) 𝑅)))
9291expd 401 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑦 ∈ (LPlanes‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ((𝑃 𝑄) 𝑅))))
9392rexlimdv 3182 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ((𝑃 𝑄) 𝑅)))
949, 93mpd 15 1 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  w3a 1098   = wceq 1634  wcel 2148  wne 2946  wrex 3065   class class class wbr 4797  cfv 6042  (class class class)co 6812  Basecbs 16084  lecple 16176  Posetcpo 17168  ltcplt 17169  joincjn 17172  Latclat 17273  ccvr 35086  Atomscatm 35087  HLchlt 35174  LPlanesclpl 35316  LVolsclvol 35317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-preset 17156  df-poset 17174  df-plt 17186  df-lub 17202  df-glb 17203  df-join 17204  df-meet 17205  df-p0 17267  df-lat 17274  df-clat 17336  df-oposet 35000  df-ol 35002  df-oml 35003  df-covers 35090  df-ats 35091  df-atl 35122  df-cvlat 35146  df-hlat 35175  df-llines 35322  df-lplanes 35323  df-lvols 35324
This theorem is referenced by:  lvolnleat  35407  lvolnlelln  35408  lvolnlelpln  35409  3atnelvolN  35410  4atlem3  35420  dalem39  35535
  Copyright terms: Public domain W3C validator