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 36144
Description: The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 36145 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 2779 . 2 (Base‘𝐾) = (Base‘𝐾)
2 2llnja.l . 2 = (le‘𝐾)
3 simpl1l 1204 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝐾 ∈ HL)
43hllatd 35942 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝐾 ∈ Lat)
5 simpl21 1231 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑄𝐴)
6 simpl22 1232 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑅𝐴)
7 2llnja.j . . . . 5 = (join‘𝐾)
8 2llnja.a . . . . 5 𝐴 = (Atoms‘𝐾)
91, 7, 8hlatjcl 35945 . . . 4 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴) → (𝑄 𝑅) ∈ (Base‘𝐾))
103, 5, 6, 9syl3anc 1351 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑄 𝑅) ∈ (Base‘𝐾))
11 simpl31 1234 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑆𝐴)
12 simpl32 1235 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑇𝐴)
131, 7, 8hlatjcl 35945 . . . 4 ((𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴) → (𝑆 𝑇) ∈ (Base‘𝐾))
143, 11, 12, 13syl3anc 1351 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 𝑇) ∈ (Base‘𝐾))
151, 7latjcl 17519 . . 3 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾)) → ((𝑄 𝑅) (𝑆 𝑇)) ∈ (Base‘𝐾))
164, 10, 14, 15syl3anc 1351 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) ∈ (Base‘𝐾))
17 simpl1r 1205 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑊𝑃)
18 2llnja.p . . . 4 𝑃 = (LPlanes‘𝐾)
191, 18lplnbase 36112 . . 3 (𝑊𝑃𝑊 ∈ (Base‘𝐾))
2017, 19syl 17 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑊 ∈ (Base‘𝐾))
21 simpr1 1174 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑄 𝑅) 𝑊)
22 simpr2 1175 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 𝑇) 𝑊)
231, 2, 7latjle12 17530 . . . 4 ((𝐾 ∈ Lat ∧ ((𝑄 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊) ↔ ((𝑄 𝑅) (𝑆 𝑇)) 𝑊))
244, 10, 14, 20, 23syl13anc 1352 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊) ↔ ((𝑄 𝑅) (𝑆 𝑇)) 𝑊))
2521, 22, 24mpbi2and 699 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) 𝑊)
261, 8atbase 35867 . . . . . . . . . 10 (𝑇𝐴𝑇 ∈ (Base‘𝐾))
2712, 26syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑇 ∈ (Base‘𝐾))
281, 7latjcl 17519 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑄 𝑅) 𝑇) ∈ (Base‘𝐾))
294, 10, 27, 28syl3anc 1351 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑇) ∈ (Base‘𝐾))
301, 8atbase 35867 . . . . . . . . . . 11 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
3111, 30syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑆 ∈ (Base‘𝐾))
321, 2, 7latlej2 17529 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 (𝑆 𝑇))
334, 31, 27, 32syl3anc 1351 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑇 (𝑆 𝑇))
341, 2, 7latjlej2 17534 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → (𝑇 (𝑆 𝑇) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇))))
354, 27, 14, 10, 34syl13anc 1352 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑇 (𝑆 𝑇) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇))))
3633, 35mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇)))
371, 2, 4, 29, 16, 20, 36, 25lattrd 17526 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑇) 𝑊)
38373adant3 1112 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) 𝑊)
39 simp11l 1264 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝐾 ∈ HL)
40 simp121 1285 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑄𝐴)
41 simp122 1286 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑅𝐴)
42 simp132 1289 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑇𝐴)
43 simp123 1287 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑄𝑅)
44 simp23 1188 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → (𝑄 𝑅) ≠ (𝑆 𝑇))
45 simpl3 1173 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → 𝑆 (𝑄 𝑅))
46 simpr 477 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → 𝑇 (𝑄 𝑅))
471, 2, 7latjle12 17530 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
484, 31, 27, 10, 47syl13anc 1352 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
49483adant3 1112 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
5049adantr 473 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → ((𝑆 (𝑄 𝑅) ∧ 𝑇 (𝑄 𝑅)) ↔ (𝑆 𝑇) (𝑄 𝑅)))
5145, 46, 50mpbi2and 699 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → (𝑆 𝑇) (𝑄 𝑅))
52 simpl3 1173 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆𝐴𝑇𝐴𝑆𝑇))
532, 7, 8ps-1 36055 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ (𝑆𝐴𝑇𝐴𝑆𝑇) ∧ (𝑄𝐴𝑅𝐴)) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
543, 52, 5, 6, 53syl112anc 1354 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
55543adant3 1112 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
5655adantr 473 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → ((𝑆 𝑇) (𝑄 𝑅) ↔ (𝑆 𝑇) = (𝑄 𝑅)))
5751, 56mpbid 224 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → (𝑆 𝑇) = (𝑄 𝑅))
5857eqcomd 2785 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) ∧ 𝑇 (𝑄 𝑅)) → (𝑄 𝑅) = (𝑆 𝑇))
5958ex 405 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → (𝑇 (𝑄 𝑅) → (𝑄 𝑅) = (𝑆 𝑇)))
6059necon3ad 2981 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) ≠ (𝑆 𝑇) → ¬ 𝑇 (𝑄 𝑅)))
6144, 60mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ¬ 𝑇 (𝑄 𝑅))
622, 7, 8, 18lplni2 36115 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑇𝐴) ∧ (𝑄𝑅 ∧ ¬ 𝑇 (𝑄 𝑅))) → ((𝑄 𝑅) 𝑇) ∈ 𝑃)
6339, 40, 41, 42, 43, 61, 62syl132anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) ∈ 𝑃)
64 simp11r 1265 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑊𝑃)
652, 18lplncmp 36140 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑄 𝑅) 𝑇) ∈ 𝑃𝑊𝑃) → (((𝑄 𝑅) 𝑇) 𝑊 ↔ ((𝑄 𝑅) 𝑇) = 𝑊))
6639, 63, 64, 65syl3anc 1351 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → (((𝑄 𝑅) 𝑇) 𝑊 ↔ ((𝑄 𝑅) 𝑇) = 𝑊))
6738, 66mpbid 224 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) = 𝑊)
68363adant3 1112 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑇) ((𝑄 𝑅) (𝑆 𝑇)))
6967, 68eqbrtrrd 4953 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ 𝑆 (𝑄 𝑅)) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇)))
70693expia 1101 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 (𝑄 𝑅) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇))))
711, 7latjcl 17519 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑄 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((𝑄 𝑅) 𝑆) ∈ (Base‘𝐾))
724, 10, 31, 71syl3anc 1351 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑆) ∈ (Base‘𝐾))
731, 2, 7latlej1 17528 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑆 (𝑆 𝑇))
744, 31, 27, 73syl3anc 1351 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑆 (𝑆 𝑇))
751, 2, 7latjlej2 17534 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑆 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 𝑅) ∈ (Base‘𝐾))) → (𝑆 (𝑆 𝑇) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇))))
764, 31, 14, 10, 75syl13anc 1352 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (𝑆 (𝑆 𝑇) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇))))
7774, 76mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇)))
781, 2, 4, 72, 16, 20, 77, 25lattrd 17526 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) 𝑆) 𝑊)
79783adant3 1112 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) 𝑊)
80 simp11l 1264 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝐾 ∈ HL)
81 simp121 1285 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑄𝐴)
82 simp122 1286 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑅𝐴)
83 simp131 1288 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑆𝐴)
84 simp123 1287 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑄𝑅)
85 simp3 1118 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ¬ 𝑆 (𝑄 𝑅))
862, 7, 8, 18lplni2 36115 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑅𝐴𝑆𝐴) ∧ (𝑄𝑅 ∧ ¬ 𝑆 (𝑄 𝑅))) → ((𝑄 𝑅) 𝑆) ∈ 𝑃)
8780, 81, 82, 83, 84, 85, 86syl132anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) ∈ 𝑃)
88 simp11r 1265 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑊𝑃)
892, 18lplncmp 36140 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑄 𝑅) 𝑆) ∈ 𝑃𝑊𝑃) → (((𝑄 𝑅) 𝑆) 𝑊 ↔ ((𝑄 𝑅) 𝑆) = 𝑊))
9080, 87, 88, 89syl3anc 1351 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → (((𝑄 𝑅) 𝑆) 𝑊 ↔ ((𝑄 𝑅) 𝑆) = 𝑊))
9179, 90mpbid 224 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) = 𝑊)
92773adant3 1112 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → ((𝑄 𝑅) 𝑆) ((𝑄 𝑅) (𝑆 𝑇)))
9391, 92eqbrtrrd 4953 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇)) ∧ ¬ 𝑆 (𝑄 𝑅)) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇)))
94933expia 1101 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → (¬ 𝑆 (𝑄 𝑅) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇))))
9570, 94pm2.61d 172 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → 𝑊 ((𝑄 𝑅) (𝑆 𝑇)))
961, 2, 4, 16, 20, 25, 95latasymd 17525 1 ((((𝐾 ∈ HL ∧ 𝑊𝑃) ∧ (𝑄𝐴𝑅𝐴𝑄𝑅) ∧ (𝑆𝐴𝑇𝐴𝑆𝑇)) ∧ ((𝑄 𝑅) 𝑊 ∧ (𝑆 𝑇) 𝑊 ∧ (𝑄 𝑅) ≠ (𝑆 𝑇))) → ((𝑄 𝑅) (𝑆 𝑇)) = 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2968   class class class wbr 4929  cfv 6188  (class class class)co 6976  Basecbs 16339  lecple 16428  joincjn 17412  Latclat 17513  Atomscatm 35841  HLchlt 35928  LLinesclln 36069  LPlanesclpl 36070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-proset 17396  df-poset 17414  df-plt 17426  df-lub 17442  df-glb 17443  df-join 17444  df-meet 17445  df-p0 17507  df-lat 17514  df-clat 17576  df-oposet 35754  df-ol 35756  df-oml 35757  df-covers 35844  df-ats 35845  df-atl 35876  df-cvlat 35900  df-hlat 35929  df-llines 36076  df-lplanes 36077
This theorem is referenced by:  2llnjN  36145
  Copyright terms: Public domain W3C validator