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 35470
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 785 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → 𝑋𝑉)
2 eqid 2764 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
3 eqid 2764 . . . . . 6 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4 eqid 2764 . . . . . 6 (LPlanes‘𝐾) = (LPlanes‘𝐾)
5 lvolnle3at.v . . . . . 6 𝑉 = (LVols‘𝐾)
62, 3, 4, 5islvol 35461 . . . . 5 (𝐾 ∈ HL → (𝑋𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
76ad2antrr 717 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑋𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
81, 7mpbid 223 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
98simprd 489 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10 oveq1 6848 . . . . . . . . 9 (𝑃 = 𝑄 → (𝑃 𝑄) = (𝑄 𝑄))
1110oveq1d 6856 . . . . . . . 8 (𝑃 = 𝑄 → ((𝑃 𝑄) 𝑅) = ((𝑄 𝑄) 𝑅))
1211breq2d 4820 . . . . . . 7 (𝑃 = 𝑄 → (𝑋 ((𝑃 𝑄) 𝑅) ↔ 𝑋 ((𝑄 𝑄) 𝑅)))
1312notbid 309 . . . . . 6 (𝑃 = 𝑄 → (¬ 𝑋 ((𝑃 𝑄) 𝑅) ↔ ¬ 𝑋 ((𝑄 𝑄) 𝑅)))
14 simp1l 1254 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
15 simp3l 1258 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LPlanes‘𝐾))
16 simp21 1263 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑃𝐴)
17 simp22 1264 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑄𝐴)
18 lvolnle3at.l . . . . . . . . . . . . 13 = (le‘𝐾)
19 lvolnle3at.j . . . . . . . . . . . . 13 = (join‘𝐾)
20 lvolnle3at.a . . . . . . . . . . . . 13 𝐴 = (Atoms‘𝐾)
2118, 19, 20, 4lplnnle2at 35429 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑃𝐴𝑄𝐴)) → ¬ 𝑦 (𝑃 𝑄))
2214, 15, 16, 17, 21syl13anc 1491 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 (𝑃 𝑄))
232, 4lplnbase 35422 . . . . . . . . . . . . . . 15 (𝑦 ∈ (LPlanes‘𝐾) → 𝑦 ∈ (Base‘𝐾))
2415, 23syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
25 simp1r 1255 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋𝑉)
262, 5lvolbase 35466 . . . . . . . . . . . . . . 15 (𝑋𝑉𝑋 ∈ (Base‘𝐾))
2725, 26syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
28 simp3r 1259 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
29 eqid 2764 . . . . . . . . . . . . . . 15 (lt‘𝐾) = (lt‘𝐾)
302, 29, 3cvrlt 35158 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
3114, 24, 27, 28, 30syl31anc 1492 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
32 hlpos 35254 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL → 𝐾 ∈ Poset)
3314, 32syl 17 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
342, 19, 20hlatjcl 35255 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
3514, 16, 17, 34syl3anc 1490 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑃 𝑄) ∈ (Base‘𝐾))
362, 18, 29pltletr 17238 . . . . . . . . . . . . . 14 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑃 𝑄)) → 𝑦(lt‘𝐾)(𝑃 𝑄)))
3733, 24, 27, 35, 36syl13anc 1491 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑃 𝑄)) → 𝑦(lt‘𝐾)(𝑃 𝑄)))
3831, 37mpand 686 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑃 𝑄) → 𝑦(lt‘𝐾)(𝑃 𝑄)))
3918, 29pltle 17228 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑃 𝑄) → 𝑦 (𝑃 𝑄)))
4014, 15, 35, 39syl3anc 1490 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑃 𝑄) → 𝑦 (𝑃 𝑄)))
4138, 40syld 47 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑃 𝑄) → 𝑦 (𝑃 𝑄)))
4222, 41mtod 189 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 (𝑃 𝑄))
4342adantr 472 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → ¬ 𝑋 (𝑃 𝑄))
44 simprr 789 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → 𝑅 (𝑃 𝑄))
4514hllatd 35252 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Lat)
46 simp23 1265 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅𝐴)
472, 20atbase 35177 . . . . . . . . . . . . . 14 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
4846, 47syl 17 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
492, 18, 19latleeqj2 17331 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
5045, 48, 35, 49syl3anc 1490 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
5150adantr 472 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → (𝑅 (𝑃 𝑄) ↔ ((𝑃 𝑄) 𝑅) = (𝑃 𝑄)))
5244, 51mpbid 223 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑅) = (𝑃 𝑄))
5352breq2d 4820 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → (𝑋 ((𝑃 𝑄) 𝑅) ↔ 𝑋 (𝑃 𝑄)))
5443, 53mtbird 316 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄))) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
5554anassrs 459 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃𝑄) ∧ 𝑅 (𝑃 𝑄)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
56 simpl1l 1293 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → 𝐾 ∈ HL)
57 simpl3l 1301 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → 𝑦 ∈ (LPlanes‘𝐾))
58 simpl2 1244 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → (𝑃𝐴𝑄𝐴𝑅𝐴))
59 simpr 477 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄)))
6018, 19, 20, 4lplni2 35425 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑅) ∈ (LPlanes‘𝐾))
6156, 58, 59, 60syl3anc 1490 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑅) ∈ (LPlanes‘𝐾))
6229, 4lplnnlt 35453 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (LPlanes‘𝐾)) → ¬ 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅))
6356, 57, 61, 62syl3anc 1490 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ¬ 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅))
642, 19latjcl 17318 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
6545, 35, 48, 64syl3anc 1490 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))
662, 18, 29pltletr 17238 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ ((𝑃 𝑄) 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 ((𝑃 𝑄) 𝑅)) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
6733, 24, 27, 65, 66syl13anc 1491 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 ((𝑃 𝑄) 𝑅)) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
6831, 67mpand 686 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ((𝑃 𝑄) 𝑅) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
6968adantr 472 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → (𝑋 ((𝑃 𝑄) 𝑅) → 𝑦(lt‘𝐾)((𝑃 𝑄) 𝑅)))
7063, 69mtod 189 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃𝑄 ∧ ¬ 𝑅 (𝑃 𝑄))) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
7170anassrs 459 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃𝑄) ∧ ¬ 𝑅 (𝑃 𝑄)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
7255, 71pm2.61dan 847 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃𝑄) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
73 eqid 2764 . . . . . . . . . 10 (le‘𝐾) = (le‘𝐾)
7473, 19, 20, 4lplnnle2at 35429 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑄𝐴𝑅𝐴)) → ¬ 𝑦(le‘𝐾)(𝑄 𝑅))
7514, 15, 17, 46, 74syl13anc 1491 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦(le‘𝐾)(𝑄 𝑅))
762, 19, 20hlatjcl 35255 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
7714, 17, 46, 76syl3anc 1490 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 𝑅) ∈ (Base‘𝐾))
782, 18, 29pltletr 17238 . . . . . . . . . . 11 ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑄 𝑅)) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
7933, 24, 27, 77, 78syl13anc 1491 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋𝑋 (𝑄 𝑅)) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
8031, 79mpand 686 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑄 𝑅) → 𝑦(lt‘𝐾)(𝑄 𝑅)))
8173, 29pltle 17228 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑄 𝑅) → 𝑦(le‘𝐾)(𝑄 𝑅)))
8214, 15, 77, 81syl3anc 1490 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑄 𝑅) → 𝑦(le‘𝐾)(𝑄 𝑅)))
8380, 82syld 47 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 (𝑄 𝑅) → 𝑦(le‘𝐾)(𝑄 𝑅)))
8475, 83mtod 189 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 (𝑄 𝑅))
8519, 20hlatjidm 35257 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑄𝐴) → (𝑄 𝑄) = 𝑄)
8614, 17, 85syl2anc 579 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 𝑄) = 𝑄)
8786oveq1d 6856 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑄 𝑄) 𝑅) = (𝑄 𝑅))
8887breq2d 4820 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ((𝑄 𝑄) 𝑅) ↔ 𝑋 (𝑄 𝑅)))
8984, 88mtbird 316 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ((𝑄 𝑄) 𝑅))
9013, 72, 89pm2.61ne 3021 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
91903expia 1150 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ((𝑃 𝑄) 𝑅)))
9291expd 404 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (𝑦 ∈ (LPlanes‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ((𝑃 𝑄) 𝑅))))
9392rexlimdv 3176 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → (∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ((𝑃 𝑄) 𝑅)))
949, 93mpd 15 1 (((𝐾 ∈ HL ∧ 𝑋𝑉) ∧ (𝑃𝐴𝑄𝐴𝑅𝐴)) → ¬ 𝑋 ((𝑃 𝑄) 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2936  wrex 3055   class class class wbr 4808  cfv 6067  (class class class)co 6841  Basecbs 16131  lecple 16222  Posetcpo 17207  ltcplt 17208  joincjn 17211  Latclat 17312  ccvr 35150  Atomscatm 35151  HLchlt 35238  LPlanesclpl 35380  LVolsclvol 35381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-proset 17195  df-poset 17213  df-plt 17225  df-lub 17241  df-glb 17242  df-join 17243  df-meet 17244  df-p0 17306  df-lat 17313  df-clat 17375  df-oposet 35064  df-ol 35066  df-oml 35067  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-llines 35386  df-lplanes 35387  df-lvols 35388
This theorem is referenced by:  lvolnleat  35471  lvolnlelln  35472  lvolnlelpln  35473  3atnelvolN  35474  4atlem3  35484  dalem39  35599
  Copyright terms: Public domain W3C validator