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

Theorem 2llnjaN 39568
Description: The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 39569 in terms of atoms). (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
2llnja.l = (le‘𝐾)
2llnja.j = (join‘𝐾)
2llnja.a 𝐴 = (Atoms‘𝐾)
2llnja.n 𝑁 = (LLines‘𝐾)
2llnja.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
2llnjaN ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) = 𝑊)

Proof of Theorem 2llnjaN
StepHypRef Expression
1 eqid 2737 . 2 (Base‘𝐾) = (Base‘𝐾)
2 2llnja.l . 2 = (le‘𝐾)
3 simpl1l 1225 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝐾 ∈ HL)
43hllatd 39365 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝐾 ∈ Lat)
5 simpl21 1252 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑄𝐴)
6 simpl22 1253 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑅𝐴)
7 2llnja.j . . . . 5 = (join‘𝐾)
8 2llnja.a . . . . 5 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 39368 . . . 4 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1373 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑄 𝑅) ∈ (Base‘𝐾))
11 simpl31 1255 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑆𝐴)
12 simpl32 1256 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑇𝐴)
131, 7, 8hlatjcl 39368 . . . 4 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
143, 11, 12, 13syl3anc 1373 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 𝑇) ∈ (Base‘𝐾))
151, 7latjcl 18484 . . 3 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑄 𝑅) (𝑆 𝑇)) ∈ (Base‘𝐾))
164, 10, 14, 15syl3anc 1373 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) ∈ (Base‘𝐾))
17 simpl1r 1226 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑊𝑃)
18 2llnja.p . . . 4 𝑃 = (LPlanes‘𝐾)
191, 18lplnbase 39536 . . 3 (𝑊𝑃𝑊 ∈ (Base‘𝐾))
2017, 19syl 17 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑊 ∈ (Base‘𝐾))
21 simpr1 1195 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑄 𝑅) 𝑊)
22 simpr2 1196 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 𝑇) 𝑊)
231, 2, 7latjle12 18495 . . . 4 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊) ↔ ((𝑄 𝑅) (𝑆 𝑇)) 𝑊))
244, 10, 14, 20, 23syl13anc 1374 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊) ↔ ((𝑄 𝑅) (𝑆 𝑇)) 𝑊))
2521, 22, 24mpbi2and 712 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) 𝑊)
261, 8atbase 39290 . . . . . . . . . 10 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
2712, 26syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑇 ∈ (Base‘𝐾))
281, 7latjcl 18484 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑄 𝑅) 𝑇) ∈ (Base‘𝐾))
294, 10, 27, 28syl3anc 1373 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑇) ∈ (Base‘𝐾))
301, 8atbase 39290 . . . . . . . . . . 11 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
3111, 30syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑆 ∈ (Base‘𝐾))
321, 2, 7latlej2 18494 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 (𝑆 𝑇))
334, 31, 27, 32syl3anc 1373 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑇 (𝑆 𝑇))
341, 2, 7latjlej2 18499 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → (𝑇 (𝑆 𝑇) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇))))
354, 27, 14, 10, 34syl13anc 1374 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑇 (𝑆 𝑇) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇))))
3633, 35mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇)))
371, 2, 4, 29, 16, 20, 36, 25lattrd 18491 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑇) 𝑊)
38373adant3 1133 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) 𝑊)
39 simp11l 1285 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝐾 ∈ HL)
40 simp121 1306 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑄𝐴)
41 simp122 1307 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑅𝐴)
42 simp132 1310 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑇𝐴)
43 simp123 1308 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑄𝑅)
44 simp23 1209 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → (𝑄 𝑅) ≠ (𝑆 𝑇))
45 simpl3 1194 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → 𝑆 (𝑄 𝑅))
46 simpr 484 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → 𝑇 (𝑄 𝑅))
471, 2, 7latjle12 18495 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
484, 31, 27, 10, 47syl13anc 1374 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
49483adant3 1133 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
5049adantr 480 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
5145, 46, 50mpbi2and 712 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → (𝑆 𝑇) (𝑄 𝑅))
52 simpl3 1194 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆𝐴𝑇𝐴𝑆𝑇))
532, 7, 8ps-1 39479 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇) ∧ (𝑄𝐴𝑅𝐴)) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
543, 52, 5, 6, 53syl112anc 1376 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
55543adant3 1133 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
5655adantr 480 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
5751, 56mpbid 232 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → (𝑆 𝑇) = (𝑄 𝑅))
5857eqcomd 2743 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → (𝑄 𝑅) = (𝑆 𝑇))
5958ex 412 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → (𝑇 (𝑄 𝑅) → (𝑄 𝑅) = (𝑆 𝑇)))
6059necon3ad 2953 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) ≠ (𝑆 𝑇) → ¬ 𝑇 (𝑄 𝑅)))
6144, 60mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ¬ 𝑇 (𝑄 𝑅))
622, 7, 8, 18lplni2 39539 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑇𝐴) ∧ (𝑄𝑅 ∧ ¬ 𝑇 (𝑄 𝑅))) → ((𝑄 𝑅) 𝑇) ∈ 𝑃)
6339, 40, 41, 42, 43, 61, 62syl132anc 1390 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) ∈ 𝑃)
64 simp11r 1286 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑊𝑃)
652, 18lplncmp 39564 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑄 𝑅) 𝑇) ∈ 𝑃𝑊𝑃) → (((𝑄 𝑅) 𝑇) 𝑊 ↔ ((𝑄 𝑅) 𝑇) = 𝑊))
6639, 63, 64, 65syl3anc 1373 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → (((𝑄 𝑅) 𝑇) 𝑊 ↔ ((𝑄 𝑅) 𝑇) = 𝑊))
6738, 66mpbid 232 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) = 𝑊)
68363adant3 1133 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇)))
6967, 68eqbrtrrd 5167 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇)))
70693expia 1122 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 (𝑄 𝑅) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇))))
711, 7latjcl 18484 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((𝑄 𝑅) 𝑆) ∈ (Base‘𝐾))
724, 10, 31, 71syl3anc 1373 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑆) ∈ (Base‘𝐾))
731, 2, 7latlej1 18493 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑆 (𝑆 𝑇))
744, 31, 27, 73syl3anc 1373 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑆 (𝑆 𝑇))
751, 2, 7latjlej2 18499 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → (𝑆 (𝑆 𝑇) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇))))
764, 31, 14, 10, 75syl13anc 1374 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 (𝑆 𝑇) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇))))
7774, 76mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇)))
781, 2, 4, 72, 16, 20, 77, 25lattrd 18491 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑆) 𝑊)
79783adant3 1133 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) 𝑊)
80 simp11l 1285 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝐾 ∈ HL)
81 simp121 1306 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑄𝐴)
82 simp122 1307 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑅𝐴)
83 simp131 1309 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑆𝐴)
84 simp123 1308 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑄𝑅)
85 simp3 1139 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ¬ 𝑆 (𝑄 𝑅))
862, 7, 8, 18lplni2 39539 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑆𝐴) ∧ (𝑄𝑅 ∧ ¬ 𝑆 (𝑄 𝑅))) → ((𝑄 𝑅) 𝑆) ∈ 𝑃)
8780, 81, 82, 83, 84, 85, 86syl132anc 1390 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) ∈ 𝑃)
88 simp11r 1286 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑊𝑃)
892, 18lplncmp 39564 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑄 𝑅) 𝑆) ∈ 𝑃𝑊𝑃) → (((𝑄 𝑅) 𝑆) 𝑊 ↔ ((𝑄 𝑅) 𝑆) = 𝑊))
9080, 87, 88, 89syl3anc 1373 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → (((𝑄 𝑅) 𝑆) 𝑊 ↔ ((𝑄 𝑅) 𝑆) = 𝑊))
9179, 90mpbid 232 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) = 𝑊)
92773adant3 1133 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇)))
9391, 92eqbrtrrd 5167 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇)))
94933expia 1122 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (¬ 𝑆 (𝑄 𝑅) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇))))
9570, 94pm2.61d 179 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇)))
961, 2, 4, 16, 20, 25, 95latasymd 18490 1 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) = 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940   class class class wbr 5143  cfv 6561  (class class class)co 7431  Basecbs 17247  lecple 17304  joincjn 18357  Latclat 18476  Atomscatm 39264  HLchlt 39351  LLinesclln 39493  LPlanesclpl 39494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-proset 18340  df-poset 18359  df-plt 18375  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-p0 18470  df-lat 18477  df-clat 18544  df-oposet 39177  df-ol 39179  df-oml 39180  df-covers 39267  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352  df-llines 39500  df-lplanes 39501
This theorem is referenced by:  2llnjN  39569
  Copyright terms: Public domain W3C validator