dalawlem15 - Mathbox for Norm Megill

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

Theorem dalawlem15 39872

Description: Lemma for dalaw 39873. Swap variable triples 𝑃𝑄𝑅 and 𝑆𝑇𝑈 in dalawlem14 39871, to obtain the elimination of the remaining conditions in dalawlem1 39858. (Contributed by NM, 6-Oct-2012.)

**Hypotheses**
Ref	Expression
dalawlem.l	⊢ ≤ = (le‘𝐾)
dalawlem.j	⊢ ∨ = (join‘𝐾)
dalawlem.m	⊢ ∧ = (meet‘𝐾)
dalawlem.a	⊢ 𝐴 = (Atoms‘𝐾)
dalawlem2.o	⊢ 𝑂 = (LPlanes‘𝐾)

**Assertion**
Ref	Expression
dalawlem15	⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))

**Proof of Theorem dalawlem15**
Step	Hyp	Ref	Expression
1		simp11 1204	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ HL)
2		simp12 1205	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))))
3		simp21 1207	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑃 ∈ 𝐴)
4		simp31 1210	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑆 ∈ 𝐴)
5		dalawlem.j	. . . . . . . . . . 11 ⊢ ∨ = (join‘𝐾)
6		dalawlem.a	. . . . . . . . . . 11 ⊢ 𝐴 = (Atoms‘𝐾)
7	5, 6	hlatjcom 39354	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) = (𝑆 ∨ 𝑃))
8	1, 3, 4, 7	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ 𝑆) = (𝑆 ∨ 𝑃))
9		simp22 1208	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑄 ∈ 𝐴)
10		simp32 1211	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑇 ∈ 𝐴)
11	5, 6	hlatjcom 39354	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑄 ∨ 𝑇) = (𝑇 ∨ 𝑄))
12	1, 9, 10, 11	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ 𝑇) = (𝑇 ∨ 𝑄))
13	8, 12	oveq12d 7387	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) = ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)))
14	13	breq1d 5112	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ↔ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑆 ∨ 𝑇)))
15	14	notbid 318	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ↔ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑆 ∨ 𝑇)))
16	13	breq1d 5112	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ↔ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑇 ∨ 𝑈)))
17	16	notbid 318	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ↔ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑇 ∨ 𝑈)))
18	13	breq1d 5112	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆) ↔ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑆)))
19	18	notbid 318	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆) ↔ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑆)))
20	15, 17, 19	3anbi123d 1438	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆)) ↔ (¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑆))))
21	20	anbi2d 630	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ↔ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑆)))))
22	2, 21	mtbid 324	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑆))))
23		simp13 1206	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈))
24	5, 6	hlatjcom 39354	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑆 ∨ 𝑃) = (𝑃 ∨ 𝑆))
25	1, 4, 3, 24	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑆 ∨ 𝑃) = (𝑃 ∨ 𝑆))
26	5, 6	hlatjcom 39354	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑇 ∨ 𝑄) = (𝑄 ∨ 𝑇))
27	1, 10, 9, 26	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑇 ∨ 𝑄) = (𝑄 ∨ 𝑇))
28	25, 27	oveq12d 7387	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) = ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)))
29		simp33 1212	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑈 ∈ 𝐴)
30		simp23 1209	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝑅 ∈ 𝐴)
31	5, 6	hlatjcom 39354	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑈 ∨ 𝑅) = (𝑅 ∨ 𝑈))
32	1, 29, 30, 31	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ∨ 𝑅) = (𝑅 ∨ 𝑈))
33	23, 28, 32	3brtr4d 5134	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑅))
34		simp3 1138	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴))
35		simp2 1137	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
36		dalawlem.l	. . . 4 ⊢ ≤ = (le‘𝐾)
37		dalawlem.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
38		dalawlem2.o	. . . 4 ⊢ 𝑂 = (LPlanes‘𝐾)
39	36, 5, 37, 6, 38	dalawlem14 39871	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑆 ∨ 𝑃) ∧ (𝑇 ∨ 𝑄)) ≤ (𝑈 ∨ 𝑅)) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≤ (((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)) ∨ ((𝑈 ∨ 𝑆) ∧ (𝑅 ∨ 𝑃))))
40	1, 22, 33, 34, 35, 39	syl311anc 1386	. 2 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)) ≤ (((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)) ∨ ((𝑈 ∨ 𝑆) ∧ (𝑅 ∨ 𝑃))))
41	1	hllatd 39350	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → 𝐾 ∈ Lat)
42		eqid 2729	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
43	42, 5, 6	hlatjcl 39353	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
44	1, 3, 9, 43	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
45	42, 5, 6	hlatjcl 39353	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
46	1, 4, 10, 45	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))
47	42, 37	latmcom 18404	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)))
48	41, 44, 46, 47	syl3anc 1373	. 2 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) = ((𝑆 ∨ 𝑇) ∧ (𝑃 ∨ 𝑄)))
49	42, 5, 6	hlatjcl 39353	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
50	1, 9, 30, 49	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
51	42, 5, 6	hlatjcl 39353	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
52	1, 10, 29, 51	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾))
53	42, 37	latmcom 18404	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)))
54	41, 50, 52, 53	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)))
55	42, 5, 6	hlatjcl 39353	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾))
56	1, 30, 3, 55	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑅 ∨ 𝑃) ∈ (Base‘𝐾))
57	42, 5, 6	hlatjcl 39353	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))
58	1, 29, 4, 57	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑈 ∨ 𝑆) ∈ (Base‘𝐾))
59	42, 37	latmcom 18404	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑃) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) = ((𝑈 ∨ 𝑆) ∧ (𝑅 ∨ 𝑃)))
60	41, 56, 58, 59	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) = ((𝑈 ∨ 𝑆) ∧ (𝑅 ∨ 𝑃)))
61	54, 60	oveq12d 7387	. 2 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))) = (((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ 𝑅)) ∨ ((𝑈 ∨ 𝑆) ∧ (𝑅 ∨ 𝑃))))
62	40, 48, 61	3brtr4d 5134	1 ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 Basecbs 17155 lecple 17203 joincjn 18252 meetcmee 18253 Latclat 18372 Atomscatm 39249 HLchlt 39336 LPlanesclpl 39479

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-1st 7947 df-2nd 7948 df-proset 18235 df-poset 18254 df-plt 18269 df-lub 18285 df-glb 18286 df-join 18287 df-meet 18288 df-p0 18364 df-lat 18373 df-clat 18440 df-oposet 39162 df-ol 39164 df-oml 39165 df-covers 39252 df-ats 39253 df-atl 39284 df-cvlat 39308 df-hlat 39337 df-llines 39485 df-lplanes 39486 df-psubsp 39490 df-pmap 39491 df-padd 39783

This theorem is referenced by: dalaw 39873

W3C validator