cdleme30a - Mathbox for Norm Megill

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

Theorem cdleme30a 40824

Description: Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.)

**Hypotheses**
Ref	Expression
cdleme30.b	⊢ 𝐵 = (Base‘𝐾)
cdleme30.l	⊢ ≤ = (le‘𝐾)
cdleme30.j	⊢ ∨ = (join‘𝐾)
cdleme30.m	⊢ ∧ = (meet‘𝐾)
cdleme30.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme30.h	⊢ 𝐻 = (LHyp‘𝐾)

**Assertion**
Ref	Expression
cdleme30a	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ (𝑌 ∧ 𝑊)) = 𝑌)

**Proof of Theorem cdleme30a**
Step	Hyp	Ref	Expression
1		simp1l 1199	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝐾 ∈ HL)
2	1	hllatd 39810	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝐾 ∈ Lat)
3		simp21 1208	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑠 ∈ 𝐴)
4		cdleme30.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
5		cdleme30.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
6	4, 5	atbase 39735	. . . 4 ⊢ (𝑠 ∈ 𝐴 → 𝑠 ∈ 𝐵)
7	3, 6	syl 17	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑠 ∈ 𝐵)
8		simp23 1210	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑌 ∈ 𝐵)
9		simp1r 1200	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑊 ∈ 𝐻)
10		cdleme30.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
11	4, 10	lhpbase 40444	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
12	9, 11	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑊 ∈ 𝐵)
13		cdleme30.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
14	4, 13	latmcl 18406	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ∈ 𝐵)
15	2, 8, 12, 14	syl3anc 1374	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑌 ∧ 𝑊) ∈ 𝐵)
16		simp22l 1294	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑋 ∈ 𝐵)
17		cdleme30.j	. . . 4 ⊢ ∨ = (join‘𝐾)
18	4, 17	latjass 18449	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑠 ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((𝑠 ∨ (𝑌 ∧ 𝑊)) ∨ 𝑋) = (𝑠 ∨ ((𝑌 ∧ 𝑊) ∨ 𝑋)))
19	2, 7, 15, 16, 18	syl13anc 1375	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → ((𝑠 ∨ (𝑌 ∧ 𝑊)) ∨ 𝑋) = (𝑠 ∨ ((𝑌 ∧ 𝑊) ∨ 𝑋)))
20		simp3l 1203	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋)
21		simp3r 1204	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑋 ≤ 𝑌)
22		cdleme30.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
23	4, 22, 13	latmlem1 18435	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊)))
24	2, 16, 8, 12, 23	syl13anc 1375	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊)))
25	21, 24	mpd 15	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊))
26	4, 13	latmcl 18406	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	2, 16, 12, 26	syl3anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
28	4, 22, 17	latjlej2 18420	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ∈ 𝐵 ∧ 𝑠 ∈ 𝐵)) → ((𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊) → (𝑠 ∨ (𝑋 ∧ 𝑊)) ≤ (𝑠 ∨ (𝑌 ∧ 𝑊))))
29	2, 27, 15, 7, 28	syl13anc 1375	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → ((𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊) → (𝑠 ∨ (𝑋 ∧ 𝑊)) ≤ (𝑠 ∨ (𝑌 ∧ 𝑊))))
30	25, 29	mpd 15	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ (𝑋 ∧ 𝑊)) ≤ (𝑠 ∨ (𝑌 ∧ 𝑊)))
31	20, 30	eqbrtrrd 5109	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑋 ≤ (𝑠 ∨ (𝑌 ∧ 𝑊)))
32	4, 17	latjcl 18405	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑠 ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ∈ 𝐵) → (𝑠 ∨ (𝑌 ∧ 𝑊)) ∈ 𝐵)
33	2, 7, 15, 32	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ (𝑌 ∧ 𝑊)) ∈ 𝐵)
34	4, 22, 17	latleeqj2 18418	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑠 ∨ (𝑌 ∧ 𝑊)) ∈ 𝐵) → (𝑋 ≤ (𝑠 ∨ (𝑌 ∧ 𝑊)) ↔ ((𝑠 ∨ (𝑌 ∧ 𝑊)) ∨ 𝑋) = (𝑠 ∨ (𝑌 ∧ 𝑊))))
35	2, 16, 33, 34	syl3anc 1374	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ≤ (𝑠 ∨ (𝑌 ∧ 𝑊)) ↔ ((𝑠 ∨ (𝑌 ∧ 𝑊)) ∨ 𝑋) = (𝑠 ∨ (𝑌 ∧ 𝑊))))
36	31, 35	mpbid 232	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → ((𝑠 ∨ (𝑌 ∧ 𝑊)) ∨ 𝑋) = (𝑠 ∨ (𝑌 ∧ 𝑊)))
37		simp1 1137	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
38	4, 22, 17, 13, 10	lhpmod2i2 40484	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑌 ∧ 𝑊) ∨ 𝑋) = (𝑌 ∧ (𝑊 ∨ 𝑋)))
39	37, 8, 16, 21, 38	syl121anc 1378	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → ((𝑌 ∧ 𝑊) ∨ 𝑋) = (𝑌 ∧ (𝑊 ∨ 𝑋)))
40	39	oveq2d 7383	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ ((𝑌 ∧ 𝑊) ∨ 𝑋)) = (𝑠 ∨ (𝑌 ∧ (𝑊 ∨ 𝑋))))
41		simp22 1209	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊))
42		eqid 2736	. . . . . . . 8 ⊢ (1.‘𝐾) = (1.‘𝐾)
43	4, 22, 17, 42, 10	lhpj1 40468	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → (𝑊 ∨ 𝑋) = (1.‘𝐾))
44	37, 41, 43	syl2anc 585	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑊 ∨ 𝑋) = (1.‘𝐾))
45	44	oveq2d 7383	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑌 ∧ (𝑊 ∨ 𝑋)) = (𝑌 ∧ (1.‘𝐾)))
46		hlol 39807	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
47	1, 46	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝐾 ∈ OL)
48	4, 13, 42	olm11 39673	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ 𝐵) → (𝑌 ∧ (1.‘𝐾)) = 𝑌)
49	47, 8, 48	syl2anc 585	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑌 ∧ (1.‘𝐾)) = 𝑌)
50	45, 49	eqtrd 2771	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑌 ∧ (𝑊 ∨ 𝑋)) = 𝑌)
51	50	oveq2d 7383	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ (𝑌 ∧ (𝑊 ∨ 𝑋))) = (𝑠 ∨ 𝑌))
52	4, 22, 17	latlej1 18414	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑠 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → 𝑠 ≤ (𝑠 ∨ (𝑋 ∧ 𝑊)))
53	2, 7, 27, 52	syl3anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑠 ≤ (𝑠 ∨ (𝑋 ∧ 𝑊)))
54	53, 20	breqtrd 5111	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑠 ≤ 𝑋)
55	4, 22, 2, 7, 16, 8, 54, 21	lattrd 18412	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → 𝑠 ≤ 𝑌)
56	4, 22, 17	latleeqj1 18417	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑠 ≤ 𝑌 ↔ (𝑠 ∨ 𝑌) = 𝑌))
57	2, 7, 8, 56	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ≤ 𝑌 ↔ (𝑠 ∨ 𝑌) = 𝑌))
58	55, 57	mpbid 232	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ 𝑌) = 𝑌)
59	40, 51, 58	3eqtrd 2775	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ ((𝑌 ∧ 𝑊) ∨ 𝑋)) = 𝑌)
60	19, 36, 59	3eqtr3d 2779	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑠 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ 𝑋 ≤ 𝑌)) → (𝑠 ∨ (𝑌 ∧ 𝑊)) = 𝑌)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 class class class wbr 5085 ‘cfv 6498 (class class class)co 7367 Basecbs 17179 lecple 17227 joincjn 18277 meetcmee 18278 1.cp1 18388 Latclat 18397 OLcol 39620 Atomscatm 39709 HLchlt 39796 LHypclh 40430

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 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 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 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-1st 7942 df-2nd 7943 df-proset 18260 df-poset 18279 df-plt 18294 df-lub 18310 df-glb 18311 df-join 18312 df-meet 18313 df-p0 18389 df-p1 18390 df-lat 18398 df-clat 18465 df-oposet 39622 df-ol 39624 df-oml 39625 df-covers 39712 df-ats 39713 df-atl 39744 df-cvlat 39768 df-hlat 39797 df-psubsp 39949 df-pmap 39950 df-padd 40242 df-lhyp 40434

This theorem is referenced by: cdleme32b 40888

W3C validator