Theorem 2llnjaN 39971

Description: The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 39972 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

Step	Hyp	Ref	Expression
1		eqid 2737	. 2 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		2llnja.l	. 2 ⊢ ≤ = (le‘𝐾)
3		simpl1l 1226	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝐾 ∈ HL)
4	3	hllatd 39769	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝐾 ∈ Lat)
5		simpl21 1253	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑄 ∈ 𝐴)
6		simpl22 1254	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑅 ∈ 𝐴)
7		2llnja.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
8		2llnja.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
9	1, 7, 8	hlatjcl 39772	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
10	3, 5, 6, 9	syl3anc 1374	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
11		simpl31 1256	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑆 ∈ 𝐴)
12		simpl32 1257	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑇 ∈ 𝐴)
13	1, 7, 8	hlatjcl 39772	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
14	3, 11, 12, 13	syl3anc 1374	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
15	1, 7	latjcl 18376	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾))
16	4, 10, 14, 15	syl3anc 1374	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾))
17		simpl1r 1227	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑊 ∈ 𝑃)
18		2llnja.p	. . . 4 ⊢ 𝑃 = (LPlanes‘𝐾)
19	1, 18	lplnbase 39939	. . 3 ⊢ (𝑊 ∈ 𝑃 → 𝑊 ∈ (Base‘𝐾))
20	17, 19	syl 17	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑊 ∈ (Base‘𝐾))
21		simpr1 1196	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑄 ∨ 𝑅) ≤ 𝑊)
22		simpr2 1197	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ∨ 𝑇) ≤ 𝑊)
23	1, 2, 7	latjle12 18387	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊) ↔ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ≤ 𝑊))
24	4, 10, 14, 20, 23	syl13anc 1375	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊) ↔ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ≤ 𝑊))
25	21, 22, 24	mpbi2and 713	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ≤ 𝑊)
26	1, 8	atbase 39694	. . . . . . . . . 10 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾))
27	12, 26	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑇 ∈ (Base‘𝐾))
28	1, 7	latjcl 18376	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ (Base‘𝐾))
29	4, 10, 27, 28	syl3anc 1374	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ (Base‘𝐾))
30	1, 8	atbase 39694	. . . . . . . . . . 11 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
31	11, 30	syl 17	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑆 ∈ (Base‘𝐾))
32	1, 2, 7	latlej2 18386	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ≤ (𝑆 ∨ 𝑇))
33	4, 31, 27, 32	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑇 ≤ (𝑆 ∨ 𝑇))
34	1, 2, 7	latjlej2 18391	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑇 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))))
35	4, 27, 14, 10, 34	syl13anc 1375	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑇 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))))
36	33, 35	mpd 15	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
37	1, 2, 4, 29, 16, 20, 36, 25	lattrd 18383	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊)
38	37	3adant3 1133	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊)
39		simp11l 1286	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝐾 ∈ HL)
40		simp121 1307	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ∈ 𝐴)
41		simp122 1308	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑅 ∈ 𝐴)
42		simp132 1311	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑇 ∈ 𝐴)
43		simp123 1309	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ≠ 𝑅)
44		simp23 1210	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))
45		simpl3 1195	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → 𝑆 ≤ (𝑄 ∨ 𝑅))
46		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → 𝑇 ≤ (𝑄 ∨ 𝑅))
47	1, 2, 7	latjle12 18387	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅)))
48	4, 31, 27, 10, 47	syl13anc 1375	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅)))
49	48	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅)))
50	49	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅)))
51	45, 46, 50	mpbi2and 713	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅))
52		simpl3 1195	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇))
53	2, 7, 8	ps-1 39882	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅)))
54	3, 52, 5, 6, 53	syl112anc 1377	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅)))
55	54	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅)))
56	55	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅)))
57	51, 56	mpbid 232	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅))
58	57	eqcomd 2743	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → (𝑄 ∨ 𝑅) = (𝑆 ∨ 𝑇))
59	58	ex 412	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (𝑇 ≤ (𝑄 ∨ 𝑅) → (𝑄 ∨ 𝑅) = (𝑆 ∨ 𝑇)))
60	59	necon3ad 2946	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇) → ¬ 𝑇 ≤ (𝑄 ∨ 𝑅)))
61	44, 60	mpd 15	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ¬ 𝑇 ≤ (𝑄 ∨ 𝑅))
62	2, 7, 8, 18	lplni2 39942	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ (𝑄 ∨ 𝑅))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ 𝑃)
63	39, 40, 41, 42, 43, 61, 62	syl132anc 1391	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ 𝑃)
64		simp11r 1287	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ∈ 𝑃)
65	2, 18	lplncmp 39967	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ 𝑃 ∧ 𝑊 ∈ 𝑃) → (((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑇) = 𝑊))
66	39, 63, 64, 65	syl3anc 1374	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑇) = 𝑊))
67	38, 66	mpbid 232	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) = 𝑊)
68	36	3adant3 1133	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
69	67, 68	eqbrtrrd 5124	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
70	69	3expia 1122	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ≤ (𝑄 ∨ 𝑅) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))))
71	1, 7	latjcl 18376	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾))
72	4, 10, 31, 71	syl3anc 1374	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾))
73	1, 2, 7	latlej1 18385	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑆 ≤ (𝑆 ∨ 𝑇))
74	4, 31, 27, 73	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑆 ≤ (𝑆 ∨ 𝑇))
75	1, 2, 7	latjlej2 18391	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑆 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))))
76	4, 31, 14, 10, 75	syl13anc 1375	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))))
77	74, 76	mpd 15	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
78	1, 2, 4, 72, 16, 20, 77, 25	lattrd 18383	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊)
79	78	3adant3 1133	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊)
80		simp11l 1286	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝐾 ∈ HL)
81		simp121 1307	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ∈ 𝐴)
82		simp122 1308	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑅 ∈ 𝐴)
83		simp131 1310	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑆 ∈ 𝐴)
84		simp123 1309	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ≠ 𝑅)
85		simp3 1139	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ¬ 𝑆 ≤ (𝑄 ∨ 𝑅))
86	2, 7, 8, 18	lplni2 39942	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑃)
87	80, 81, 82, 83, 84, 85, 86	syl132anc 1391	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑃)
88		simp11r 1287	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ∈ 𝑃)
89	2, 18	lplncmp 39967	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑃 ∧ 𝑊 ∈ 𝑃) → (((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑆) = 𝑊))
90	80, 87, 88, 89	syl3anc 1374	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑆) = 𝑊))
91	79, 90	mpbid 232	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) = 𝑊)
92	77	3adant3 1133	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
93	91, 92	eqbrtrrd 5124	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
94	93	3expia 1122	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (¬ 𝑆 ≤ (𝑄 ∨ 𝑅) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))))
95	70, 94	pm2.61d 179	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))
96	1, 2, 4, 16, 20, 25, 95	latasymd 18382	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) = 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5100  ‘cfv 6502  (class class class)co 7370  Basecbs 17150  lecple 17198  joincjn 18248  Latclat 18368  Atomscatm 39668  HLchlt 39755  LLinesclln 39896  LPlanesclpl 39897

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-proset 18231  df-poset 18250  df-plt 18265  df-lub 18281  df-glb 18282  df-join 18283  df-meet 18284  df-p0 18360  df-lat 18369  df-clat 18436  df-oposet 39581  df-ol 39583  df-oml 39584  df-covers 39671  df-ats 39672  df-atl 39703  df-cvlat 39727  df-hlat 39756  df-llines 39903  df-lplanes 39904

This theorem is referenced by:  2llnjN  39972