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

Theorem ps-2 36773
Description: Lattice analogue for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in [MaedaMaeda] p. 68 and part of Theorem 16.4 in [MaedaMaeda] p. 69. (Contributed by NM, 1-Dec-2011.)
Hypotheses
Ref Expression
ps1.l = (le‘𝐾)
ps1.j = (join‘𝐾)
ps1.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
ps-2 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇)))
Distinct variable groups:   𝑢,𝐴   𝑢,   𝑢,𝐾   𝑢,   𝑢,𝑃   𝑢,𝑄   𝑢,𝑅   𝑢,𝑆   𝑢,𝑇

Proof of Theorem ps-2
StepHypRef Expression
1 simpl21 1248 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆 = 𝑃) → 𝑃𝐴)
2 simp1 1133 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝐾 ∈ HL)
3 simp21 1203 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑃𝐴)
4 simp23 1205 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑅𝐴)
5 ps1.l . . . . . . . 8 = (le‘𝐾)
6 ps1.j . . . . . . . 8 = (join‘𝐾)
7 ps1.a . . . . . . . 8 𝐴 = (Atoms‘𝐾)
85, 6, 7hlatlej1 36670 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴) → 𝑃 (𝑃 𝑅))
92, 3, 4, 8syl3anc 1368 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑃 (𝑃 𝑅))
109adantr 484 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆 = 𝑃) → 𝑃 (𝑃 𝑅))
11 simp3r 1199 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑇𝐴)
125, 6, 7hlatlej1 36670 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑇𝐴) → 𝑃 (𝑃 𝑇))
132, 3, 11, 12syl3anc 1368 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑃 (𝑃 𝑇))
14 oveq1 7146 . . . . . . . 8 (𝑆 = 𝑃 → (𝑆 𝑇) = (𝑃 𝑇))
1514breq2d 5045 . . . . . . 7 (𝑆 = 𝑃 → (𝑃 (𝑆 𝑇) ↔ 𝑃 (𝑃 𝑇)))
1613, 15syl5ibrcom 250 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑆 = 𝑃𝑃 (𝑆 𝑇)))
1716imp 410 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆 = 𝑃) → 𝑃 (𝑆 𝑇))
18 breq1 5036 . . . . . . 7 (𝑢 = 𝑃 → (𝑢 (𝑃 𝑅) ↔ 𝑃 (𝑃 𝑅)))
19 breq1 5036 . . . . . . 7 (𝑢 = 𝑃 → (𝑢 (𝑆 𝑇) ↔ 𝑃 (𝑆 𝑇)))
2018, 19anbi12d 633 . . . . . 6 (𝑢 = 𝑃 → ((𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇)) ↔ (𝑃 (𝑃 𝑅) ∧ 𝑃 (𝑆 𝑇))))
2120rspcev 3574 . . . . 5 ((𝑃𝐴 ∧ (𝑃 (𝑃 𝑅) ∧ 𝑃 (𝑆 𝑇))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇)))
221, 10, 17, 21syl12anc 835 . . . 4 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆 = 𝑃) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇)))
2322a1d 25 . . 3 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆 = 𝑃) → (((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
24 hlop 36657 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ HL → 𝐾 ∈ OP)
25243ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝐾 ∈ OP)
26 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Base‘𝐾) = (Base‘𝐾)
27 eqid 2801 . . . . . . . . . . . . . . . . . 18 (0.‘𝐾) = (0.‘𝐾)
2826, 27op0cl 36479 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
2925, 28syl 17 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (0.‘𝐾) ∈ (Base‘𝐾))
3026, 7atbase 36584 . . . . . . . . . . . . . . . . 17 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
313, 30syl 17 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑃 ∈ (Base‘𝐾))
32 eqid 2801 . . . . . . . . . . . . . . . . . 18 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
3327, 32, 7atcvr0 36583 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ 𝑃𝐴) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
342, 3, 33syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (0.‘𝐾)( ⋖ ‘𝐾)𝑃)
35 eqid 2801 . . . . . . . . . . . . . . . . 17 (lt‘𝐾) = (lt‘𝐾)
3626, 35, 32cvrlt 36565 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃) → (0.‘𝐾)(lt‘𝐾)𝑃)
372, 29, 31, 34, 36syl31anc 1370 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (0.‘𝐾)(lt‘𝐾)𝑃)
38 hlpos 36661 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ HL → 𝐾 ∈ Poset)
39383ad2ant1 1130 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝐾 ∈ Poset)
40 hllat 36658 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ HL → 𝐾 ∈ Lat)
41403ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝐾 ∈ Lat)
4226, 7atbase 36584 . . . . . . . . . . . . . . . . . 18 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
434, 42syl 17 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑅 ∈ (Base‘𝐾))
4426, 6latjcl 17657 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑃 𝑅) ∈ (Base‘𝐾))
4541, 31, 43, 44syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑃 𝑅) ∈ (Base‘𝐾))
4626, 5, 35pltletr 17577 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ Poset ∧ ((0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑃 𝑅) ∈ (Base‘𝐾))) → (((0.‘𝐾)(lt‘𝐾)𝑃𝑃 (𝑃 𝑅)) → (0.‘𝐾)(lt‘𝐾)(𝑃 𝑅)))
4739, 29, 31, 45, 46syl13anc 1369 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (((0.‘𝐾)(lt‘𝐾)𝑃𝑃 (𝑃 𝑅)) → (0.‘𝐾)(lt‘𝐾)(𝑃 𝑅)))
4837, 9, 47mp2and 698 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (0.‘𝐾)(lt‘𝐾)(𝑃 𝑅))
4935pltne 17568 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ (Base‘𝐾) ∧ (𝑃 𝑅) ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)(𝑃 𝑅) → (0.‘𝐾) ≠ (𝑃 𝑅)))
502, 29, 45, 49syl3anc 1368 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → ((0.‘𝐾)(lt‘𝐾)(𝑃 𝑅) → (0.‘𝐾) ≠ (𝑃 𝑅)))
5148, 50mpd 15 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (0.‘𝐾) ≠ (𝑃 𝑅))
5251necomd 3045 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑃 𝑅) ≠ (0.‘𝐾))
5352adantr 484 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → (𝑃 𝑅) ≠ (0.‘𝐾))
54 hlatl 36655 . . . . . . . . . . . . . . . . . . 19 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
55543ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝐾 ∈ AtLat)
56 simp3l 1198 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑆𝐴)
575, 7atncmp 36607 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ AtLat ∧ 𝑆𝐴𝑃𝐴) → (¬ 𝑆 𝑃𝑆𝑃))
5855, 56, 3, 57syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (¬ 𝑆 𝑃𝑆𝑃))
59 simp22 1204 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑄𝐴)
6026, 5, 6, 7hlexch1 36677 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑄𝐴𝑃 ∈ (Base‘𝐾)) ∧ ¬ 𝑆 𝑃) → (𝑆 (𝑃 𝑄) → 𝑄 (𝑃 𝑆)))
61603expia 1118 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑄𝐴𝑃 ∈ (Base‘𝐾))) → (¬ 𝑆 𝑃 → (𝑆 (𝑃 𝑄) → 𝑄 (𝑃 𝑆))))
622, 56, 59, 31, 61syl13anc 1369 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (¬ 𝑆 𝑃 → (𝑆 (𝑃 𝑄) → 𝑄 (𝑃 𝑆))))
6358, 62sylbird 263 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑆𝑃 → (𝑆 (𝑃 𝑄) → 𝑄 (𝑃 𝑆))))
6463imp32 422 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃𝑆 (𝑃 𝑄))) → 𝑄 (𝑃 𝑆))
6526, 7atbase 36584 . . . . . . . . . . . . . . . . . 18 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
6659, 65syl 17 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑄 ∈ (Base‘𝐾))
6726, 7atbase 36584 . . . . . . . . . . . . . . . . . . 19 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
6856, 67syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑆 ∈ (Base‘𝐾))
6926, 6latjcl 17657 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑃 𝑆) ∈ (Base‘𝐾))
7041, 31, 68, 69syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑃 𝑆) ∈ (Base‘𝐾))
7126, 5, 6latjlej1 17671 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾))) → (𝑄 (𝑃 𝑆) → (𝑄 𝑅) ((𝑃 𝑆) 𝑅)))
7241, 66, 70, 43, 71syl13anc 1369 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑄 (𝑃 𝑆) → (𝑄 𝑅) ((𝑃 𝑆) 𝑅)))
7372adantr 484 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃𝑆 (𝑃 𝑄))) → (𝑄 (𝑃 𝑆) → (𝑄 𝑅) ((𝑃 𝑆) 𝑅)))
7464, 73mpd 15 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃𝑆 (𝑃 𝑄))) → (𝑄 𝑅) ((𝑃 𝑆) 𝑅))
7574adantrrr 724 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → (𝑄 𝑅) ((𝑃 𝑆) 𝑅))
7626, 7atbase 36584 . . . . . . . . . . . . . . . . . 18 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
7711, 76syl 17 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → 𝑇 ∈ (Base‘𝐾))
7826, 6latjcl 17657 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑄 𝑅) ∈ (Base‘𝐾))
7941, 66, 43, 78syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑄 𝑅) ∈ (Base‘𝐾))
8026, 6latjcl 17657 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ (𝑃 𝑆) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 𝑆) 𝑅) ∈ (Base‘𝐾))
8141, 70, 43, 80syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → ((𝑃 𝑆) 𝑅) ∈ (Base‘𝐾))
8226, 5lattr 17662 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ ((𝑃 𝑆) 𝑅) ∈ (Base‘𝐾))) → ((𝑇 (𝑄 𝑅) ∧ (𝑄 𝑅) ((𝑃 𝑆) 𝑅)) → 𝑇 ((𝑃 𝑆) 𝑅)))
8341, 77, 79, 81, 82syl13anc 1369 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → ((𝑇 (𝑄 𝑅) ∧ (𝑄 𝑅) ((𝑃 𝑆) 𝑅)) → 𝑇 ((𝑃 𝑆) 𝑅)))
8483expdimp 456 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑇 (𝑄 𝑅)) → ((𝑄 𝑅) ((𝑃 𝑆) 𝑅) → 𝑇 ((𝑃 𝑆) 𝑅)))
8584adantrl 715 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅))) → ((𝑄 𝑅) ((𝑃 𝑆) 𝑅) → 𝑇 ((𝑃 𝑆) 𝑅)))
8685adantrl 715 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ((𝑄 𝑅) ((𝑃 𝑆) 𝑅) → 𝑇 ((𝑃 𝑆) 𝑅)))
8775, 86mpd 15 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → 𝑇 ((𝑃 𝑆) 𝑅))
886, 7hlatj32 36667 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑆𝐴𝑅𝐴)) → ((𝑃 𝑆) 𝑅) = ((𝑃 𝑅) 𝑆))
892, 3, 56, 4, 88syl13anc 1369 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → ((𝑃 𝑆) 𝑅) = ((𝑃 𝑅) 𝑆))
9089breq2d 5045 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (𝑇 ((𝑃 𝑆) 𝑅) ↔ 𝑇 ((𝑃 𝑅) 𝑆)))
9190adantr 484 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → (𝑇 ((𝑃 𝑆) 𝑅) ↔ 𝑇 ((𝑃 𝑅) 𝑆)))
9287, 91mpbid 235 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → 𝑇 ((𝑃 𝑅) 𝑆))
9353, 92jca 515 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ((𝑃 𝑅) ≠ (0.‘𝐾) ∧ 𝑇 ((𝑃 𝑅) 𝑆)))
9493adantrrl 723 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (𝑆𝑃 ∧ (¬ 𝑃 (𝑄 𝑅) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅))))) → ((𝑃 𝑅) ≠ (0.‘𝐾) ∧ 𝑇 ((𝑃 𝑅) 𝑆)))
9594ex 416 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → ((𝑆𝑃 ∧ (¬ 𝑃 (𝑄 𝑅) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ((𝑃 𝑅) ≠ (0.‘𝐾) ∧ 𝑇 ((𝑃 𝑅) 𝑆))))
9626, 5, 6, 27, 7cvrat4 36738 . . . . . . . . 9 ((𝐾 ∈ HL ∧ ((𝑃 𝑅) ∈ (Base‘𝐾) ∧ 𝑇𝐴𝑆𝐴)) → (((𝑃 𝑅) ≠ (0.‘𝐾) ∧ 𝑇 ((𝑃 𝑅) 𝑆)) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢))))
972, 45, 11, 56, 96syl13anc 1369 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (((𝑃 𝑅) ≠ (0.‘𝐾) ∧ 𝑇 ((𝑃 𝑅) 𝑆)) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢))))
9895, 97syld 47 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → ((𝑆𝑃 ∧ (¬ 𝑃 (𝑄 𝑅) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢))))
9998impl 459 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑃) ∧ (¬ 𝑃 (𝑄 𝑅) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢)))
10099adantrlr 722 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑃) ∧ ((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢)))
1015, 7atncmp 36607 . . . . . . . . . . . . . . 15 ((𝐾 ∈ AtLat ∧ 𝑇𝐴𝑆𝐴) → (¬ 𝑇 𝑆𝑇𝑆))
10255, 11, 56, 101syl3anc 1368 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (¬ 𝑇 𝑆𝑇𝑆))
103 necom 3043 . . . . . . . . . . . . . 14 (𝑇𝑆𝑆𝑇)
104102, 103syl6bb 290 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (¬ 𝑇 𝑆𝑆𝑇))
105104adantr 484 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → (¬ 𝑇 𝑆𝑆𝑇))
106 simpl1 1188 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → 𝐾 ∈ HL)
107 simpl3r 1226 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → 𝑇𝐴)
108 simpr 488 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → 𝑢𝐴)
10968adantr 484 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → 𝑆 ∈ (Base‘𝐾))
11026, 5, 6, 7hlexch1 36677 . . . . . . . . . . . . . 14 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑢𝐴𝑆 ∈ (Base‘𝐾)) ∧ ¬ 𝑇 𝑆) → (𝑇 (𝑆 𝑢) → 𝑢 (𝑆 𝑇)))
1111103expia 1118 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝑇𝐴𝑢𝐴𝑆 ∈ (Base‘𝐾))) → (¬ 𝑇 𝑆 → (𝑇 (𝑆 𝑢) → 𝑢 (𝑆 𝑇))))
112106, 107, 108, 109, 111syl13anc 1369 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → (¬ 𝑇 𝑆 → (𝑇 (𝑆 𝑢) → 𝑢 (𝑆 𝑇))))
113105, 112sylbird 263 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) → (𝑆𝑇 → (𝑇 (𝑆 𝑢) → 𝑢 (𝑆 𝑇))))
114113imp 410 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑢𝐴) ∧ 𝑆𝑇) → (𝑇 (𝑆 𝑢) → 𝑢 (𝑆 𝑇)))
115114an32s 651 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑇) ∧ 𝑢𝐴) → (𝑇 (𝑆 𝑢) → 𝑢 (𝑆 𝑇)))
116115anim2d 614 . . . . . . . 8 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑇) ∧ 𝑢𝐴) → ((𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢)) → (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
117116reximdva 3236 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑇) → (∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢)) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
118117ad2ant2rl 748 . . . . . 6 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑃) ∧ (¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇)) → (∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢)) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
119118adantrr 716 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑃) ∧ ((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → (∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑇 (𝑆 𝑢)) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
120100, 119mpd 15 . . . 4 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑃) ∧ ((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇)))
121120ex 416 . . 3 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ 𝑆𝑃) → (((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
12223, 121pm2.61dane 3077 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) → (((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇))))
123122imp 410 1 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ ((¬ 𝑃 (𝑄 𝑅) ∧ 𝑆𝑇) ∧ (𝑆 (𝑃 𝑄) ∧ 𝑇 (𝑄 𝑅)))) → ∃𝑢𝐴 (𝑢 (𝑃 𝑅) ∧ 𝑢 (𝑆 𝑇)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wrex 3110   class class class wbr 5033  cfv 6328  (class class class)co 7139  Basecbs 16479  lecple 16568  Posetcpo 17546  ltcplt 17547  joincjn 17550  0.cp0 17643  Latclat 17651  OPcops 36467  ccvr 36557  Atomscatm 36558  AtLatcal 36559  HLchlt 36645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-proset 17534  df-poset 17552  df-plt 17564  df-lub 17580  df-glb 17581  df-join 17582  df-meet 17583  df-p0 17645  df-lat 17652  df-clat 17714  df-oposet 36471  df-ol 36473  df-oml 36474  df-covers 36561  df-ats 36562  df-atl 36593  df-cvlat 36617  df-hlat 36646
This theorem is referenced by:  ps-2b  36777  paddasslem3  37117
  Copyright terms: Public domain W3C validator