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 40329

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 1285	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
3		hlol 39340	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
4	2, 3	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ OL)
5		simp12l 1287	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ∈ 𝐴)
6		simp13l 1289	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑇 ∈ 𝐴)
7		cdleme23.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
8		cdleme23.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
9		cdleme23.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
10	7, 8, 9	hlatjcl 39346	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ 𝐵)
11	2, 5, 6, 10	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ 𝑇) ∈ 𝐵)
12	2	hllatd 39343	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
13		simp2l 1200	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
14		simp11r 1286	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
15		cdleme23.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
16	7, 15	lhpbase 39977	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
17	14, 16	syl 17	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
18		cdleme23.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
19	7, 18	latmcl 18346	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
20	12, 13, 17, 19	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
21	7, 8	latjcl 18345	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)
22	12, 11, 20, 21	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)
23	7, 18	latmassOLD 39208	. . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((𝑆 ∨ 𝑇) ∈ 𝐵 ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)))
24	4, 11, 22, 17, 23	syl13anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)))
25		cdleme23.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
26	7, 25, 8	latlej1 18354	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)))
27	12, 11, 20, 26	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)))
28	7, 25, 18	latleeqm1 18373	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵) → ((𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ↔ ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇)))
29	12, 11, 22, 28	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ↔ ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇)))
30	27, 29	mpbid 232	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇))
31	30	oveq1d 7364	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ 𝑊))
32	7, 9	atbase 39268	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐵)
33	5, 32	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ∈ 𝐵)
34	7, 9	atbase 39268	. . . . . . . . 9 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ 𝐵)
35	6, 34	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑇 ∈ 𝐵)
36	7, 8	latjjdir 18398	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))))
37	12, 33, 35, 20, 36	syl13anc 1374	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))))
38		simp32 1211	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
39		simp33 1212	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
40	38, 39	oveq12d 7367	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))) = (𝑋 ∨ 𝑋))
41	7, 8	latjidm 18368	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
42	12, 13, 41	syl2anc 584	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∨ 𝑋) = 𝑋)
43	37, 40, 42	3eqtrd 2768	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = 𝑋)
44	43	oveq1d 7364	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊) = (𝑋 ∧ 𝑊))
45	44	oveq2d 7365	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)) = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)))
46	24, 31, 45	3eqtr3d 2772	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)))
47		simp12r 1288	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ¬ 𝑆 ≤ 𝑊)
48		simp31 1210	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ≠ 𝑇)
49	25, 8, 18, 9, 15	lhpat 40022	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴)
50	2, 14, 5, 47, 6, 48, 49	syl222anc 1388	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴)
51	46, 50	eqeltrrd 2829	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)) ∈ 𝐴)
52	1, 51	eqeltrid 2832	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑉 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5092 ‘cfv 6482 (class class class)co 7349 Basecbs 17120 lecple 17168 joincjn 18217 meetcmee 18218 Latclat 18337 OLcol 39153 Atomscatm 39242 HLchlt 39329 LHypclh 39963

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 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 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 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-proset 18200 df-poset 18219 df-plt 18234 df-lub 18250 df-glb 18251 df-join 18252 df-meet 18253 df-p0 18329 df-p1 18330 df-lat 18338 df-clat 18405 df-oposet 39155 df-ol 39157 df-oml 39158 df-covers 39245 df-ats 39246 df-atl 39277 df-cvlat 39301 df-hlat 39330 df-lhyp 39967

This theorem is referenced by: cdleme28a 40349

W3C validator