cdleme23b - Mathbox for Norm Megill

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

Theorem cdleme23b 40842

Description: Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)

**Hypotheses**
Ref	Expression
cdleme23.b	⊢ 𝐵 = (Base‘𝐾)
cdleme23.l	⊢ ≤ = (le‘𝐾)
cdleme23.j	⊢ ∨ = (join‘𝐾)
cdleme23.m	⊢ ∧ = (meet‘𝐾)
cdleme23.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme23.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme23.v	⊢ 𝑉 = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊))

**Assertion**
Ref	Expression
cdleme23b	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑉 ∈ 𝐴)

**Proof of Theorem cdleme23b**
Step	Hyp	Ref	Expression
1		cdleme23.v	. 2 ⊢ 𝑉 = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊))
2		simp11l 1291	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
3		hlol 39853	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
4	2, 3	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ OL)
5		simp12l 1293	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ∈ 𝐴)
6		simp13l 1295	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑇 ∈ 𝐴)
7		cdleme23.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
8		cdleme23.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
9		cdleme23.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
10	7, 8, 9	hlatjcl 39859	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ 𝐵)
11	2, 5, 6, 10	syl3anc 1379	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ 𝑇) ∈ 𝐵)
12	2	hllatd 39856	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
13		simp2l 1206	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
14		simp11r 1292	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
15		cdleme23.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
16	7, 15	lhpbase 40490	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
17	14, 16	syl 17	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
18		cdleme23.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
19	7, 18	latmcl 18397	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
20	12, 13, 17, 19	syl3anc 1379	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
21	7, 8	latjcl 18396	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)
22	12, 11, 20, 21	syl3anc 1379	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)
23	7, 18	latmassOLD 39721	. . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((𝑆 ∨ 𝑇) ∈ 𝐵 ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)))
24	4, 11, 22, 17, 23	syl13anc 1380	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)))
25		cdleme23.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
26	7, 25, 8	latlej1 18405	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)))
27	12, 11, 20, 26	syl3anc 1379	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)))
28	7, 25, 18	latleeqm1 18424	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵) → ((𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ↔ ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇)))
29	12, 11, 22, 28	syl3anc 1379	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ↔ ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇)))
30	27, 29	mpbid 233	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇))
31	30	oveq1d 7371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ 𝑊))
32	7, 9	atbase 39781	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐵)
33	5, 32	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ∈ 𝐵)
34	7, 9	atbase 39781	. . . . . . . . 9 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ 𝐵)
35	6, 34	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑇 ∈ 𝐵)
36	7, 8	latjjdir 18449	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))))
37	12, 33, 35, 20, 36	syl13anc 1380	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))))
38		simp32 1217	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
39		simp33 1218	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
40	38, 39	oveq12d 7374	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))) = (𝑋 ∨ 𝑋))
41	7, 8	latjidm 18419	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
42	12, 13, 41	syl2anc 590	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∨ 𝑋) = 𝑋)
43	37, 40, 42	3eqtrd 2778	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = 𝑋)
44	43	oveq1d 7371	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊) = (𝑋 ∧ 𝑊))
45	44	oveq2d 7372	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)) = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)))
46	24, 31, 45	3eqtr3d 2782	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)))
47		simp12r 1294	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ¬ 𝑆 ≤ 𝑊)
48		simp31 1216	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ≠ 𝑇)
49	25, 8, 18, 9, 15	lhpat 40535	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴)
50	2, 14, 5, 47, 6, 48, 49	syl222anc 1394	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴)
51	46, 50	eqeltrrd 2840	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)) ∈ 𝐴)
52	1, 51	eqeltrid 2843	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑉 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 class class class wbr 5072 ‘cfv 6485 (class class class)co 7356 Basecbs 17170 lecple 17218 joincjn 18268 meetcmee 18269 Latclat 18388 OLcol 39666 Atomscatm 39755 HLchlt 39842 LHypclh 40476

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-proset 18251 df-poset 18270 df-plt 18285 df-lub 18301 df-glb 18302 df-join 18303 df-meet 18304 df-p0 18380 df-p1 18381 df-lat 18389 df-clat 18456 df-oposet 39668 df-ol 39670 df-oml 39671 df-covers 39758 df-ats 39759 df-atl 39790 df-cvlat 39814 df-hlat 39843 df-lhyp 40480

This theorem is referenced by: cdleme28a 40862

W3C validator