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 40974

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 1298	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
3		hlol 39985	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
4	2, 3	syl 17	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ OL)
5		simp12l 1300	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ∈ 𝐴)
6		simp13l 1302	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑇 ∈ 𝐴)
7		cdleme23.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
8		cdleme23.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
9		cdleme23.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
10	7, 8, 9	hlatjcl 39991	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ 𝐵)
11	2, 5, 6, 10	syl3anc 1390	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ 𝑇) ∈ 𝐵)
12	2	hllatd 39988	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
13		simp2l 1213	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
14		simp11r 1299	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
15		cdleme23.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
16	7, 15	lhpbase 40622	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
17	14, 16	syl 17	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
18		cdleme23.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
19	7, 18	latmcl 18472	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
20	12, 13, 17, 19	syl3anc 1390	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
21	7, 8	latjcl 18471	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)
22	12, 11, 20, 21	syl3anc 1390	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵)
23	7, 18	latmassOLD 39853	. . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((𝑆 ∨ 𝑇) ∈ 𝐵 ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)))
24	4, 11, 22, 17, 23	syl13anc 1391	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)))
25		cdleme23.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
26	7, 25, 8	latlej1 18480	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)))
27	12, 11, 20, 26	syl3anc 1390	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)))
28	7, 25, 18	latleeqm1 18499	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ 𝐵 ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵) → ((𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ↔ ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇)))
29	12, 11, 22, 28	syl3anc 1390	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ≤ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ↔ ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇)))
30	27, 29	mpbid 234	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) = (𝑆 ∨ 𝑇))
31	30	oveq1d 7411	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∧ ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊))) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ 𝑊))
32	7, 9	atbase 39913	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐵)
33	5, 32	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ∈ 𝐵)
34	7, 9	atbase 39913	. . . . . . . . 9 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ 𝐵)
35	6, 34	syl 17	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑇 ∈ 𝐵)
36	7, 8	latjjdir 18524	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))))
37	12, 33, 35, 20, 36	syl13anc 1391	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))))
38		simp32 1224	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
39		simp33 1225	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
40	38, 39	oveq12d 7414	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ (𝑋 ∧ 𝑊)) ∨ (𝑇 ∨ (𝑋 ∧ 𝑊))) = (𝑋 ∨ 𝑋))
41	7, 8	latjidm 18494	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 𝑋) = 𝑋)
42	12, 13, 41	syl2anc 593	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∨ 𝑋) = 𝑋)
43	37, 40, 42	3eqtrd 2801	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) = 𝑋)
44	43	oveq1d 7411	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊) = (𝑋 ∧ 𝑊))
45	44	oveq2d 7412	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ (((𝑆 ∨ 𝑇) ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊)) = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)))
46	24, 31, 45	3eqtr3d 2805	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) = ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)))
47		simp12r 1301	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ¬ 𝑆 ≤ 𝑊)
48		simp31 1223	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑆 ≠ 𝑇)
49	25, 8, 18, 9, 15	lhpat 40667	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴)
50	2, 14, 5, 47, 6, 48, 49	syl222anc 1405	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴)
51	46, 50	eqeltrrd 2863	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((𝑆 ∨ 𝑇) ∧ (𝑋 ∧ 𝑊)) ∈ 𝐴)
52	1, 51	eqeltrid 2866	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑆 ≠ 𝑇 ∧ (𝑆 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑇 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑉 ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 ≠ wne 2957 class class class wbr 5100 ‘cfv 6521 (class class class)co 7396 Basecbs 17245 lecple 17293 joincjn 18343 meetcmee 18344 Latclat 18463 OLcol 39798 Atomscatm 39887 HLchlt 39974 LHypclh 40608

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5542 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-proset 18326 df-poset 18345 df-plt 18360 df-lub 18376 df-glb 18377 df-join 18378 df-meet 18379 df-p0 18455 df-p1 18456 df-lat 18464 df-clat 18531 df-oposet 39800 df-ol 39802 df-oml 39803 df-covers 39890 df-ats 39891 df-atl 39922 df-cvlat 39946 df-hlat 39975 df-lhyp 40612

This theorem is referenced by: cdleme28a 40994

W3C validator