cdleme20c - Mathbox for Norm Megill

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

Theorem cdleme20c 40356

Description: Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. 𝐷, 𝐹, 𝑌, 𝐺 represent s₂, f(s), t₂, f(t). (Contributed by NM, 15-Nov-2012.)

**Hypotheses**
Ref	Expression
cdleme19.l	⊢ ≤ = (le‘𝐾)
cdleme19.j	⊢ ∨ = (join‘𝐾)
cdleme19.m	⊢ ∧ = (meet‘𝐾)
cdleme19.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme19.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme19.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme19.f	⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
cdleme19.g	⊢ 𝐺 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ 𝑊)))
cdleme19.d	⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊)
cdleme19.y	⊢ 𝑌 = ((𝑅 ∨ 𝑇) ∧ 𝑊)
cdleme20.v	⊢ 𝑉 = ((𝑆 ∨ 𝑇) ∧ 𝑊)

**Assertion**
Ref	Expression
cdleme20c	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝐷 ∨ 𝑌) = (((𝑅 ∨ 𝑆) ∨ 𝑇) ∧ 𝑊))

**Proof of Theorem cdleme20c**
Step	Hyp	Ref	Expression
1		cdleme19.d	. . 3 ⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊)
2		cdleme19.y	. . 3 ⊢ 𝑌 = ((𝑅 ∨ 𝑇) ∧ 𝑊)
3	1, 2	oveq12i 7358	. 2 ⊢ (𝐷 ∨ 𝑌) = (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ ((𝑅 ∨ 𝑇) ∧ 𝑊))
4		simp1l 1198	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ HL)
5		simp21l 1291	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ∈ 𝐴)
6		simp22l 1293	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑆 ∈ 𝐴)
7		eqid 2731	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
8		cdleme19.j	. . . . . . . . . 10 ⊢ ∨ = (join‘𝐾)
9		cdleme19.a	. . . . . . . . . 10 ⊢ 𝐴 = (Atoms‘𝐾)
10	7, 8, 9	hlatjcl 39412	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
11	4, 5, 6, 10	syl3anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
12		simp1r 1199	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑊 ∈ 𝐻)
13		cdleme19.h	. . . . . . . . . 10 ⊢ 𝐻 = (LHyp‘𝐾)
14	7, 13	lhpbase 40043	. . . . . . . . 9 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
15	12, 14	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑊 ∈ (Base‘𝐾))
16		cdleme19.l	. . . . . . . . . 10 ⊢ ≤ = (le‘𝐾)
17	16, 8, 9	hlatlej1 39420	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → 𝑅 ≤ (𝑅 ∨ 𝑆))
18	4, 5, 6, 17	syl3anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑅 ∨ 𝑆))
19		cdleme19.m	. . . . . . . . 9 ⊢ ∧ = (meet‘𝐾)
20	7, 16, 8, 19, 9	atmod2i1 39906	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑅 ≤ (𝑅 ∨ 𝑆)) → (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ 𝑅) = ((𝑅 ∨ 𝑆) ∧ (𝑊 ∨ 𝑅)))
21	4, 5, 11, 15, 18, 20	syl131anc 1385	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ 𝑅) = ((𝑅 ∨ 𝑆) ∧ (𝑊 ∨ 𝑅)))
22		simp21 1207	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
23		eqid 2731	. . . . . . . . . 10 ⊢ (1.‘𝐾) = (1.‘𝐾)
24	16, 8, 23, 9, 13	lhpjat1 40065	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑊 ∨ 𝑅) = (1.‘𝐾))
25	4, 12, 22, 24	syl21anc 837	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑊 ∨ 𝑅) = (1.‘𝐾))
26	25	oveq2d 7362	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∧ (𝑊 ∨ 𝑅)) = ((𝑅 ∨ 𝑆) ∧ (1.‘𝐾)))
27		hlol 39406	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
28	4, 27	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ OL)
29	7, 19, 23	olm11 39272	. . . . . . . 8 ⊢ ((𝐾 ∈ OL ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑆) ∧ (1.‘𝐾)) = (𝑅 ∨ 𝑆))
30	28, 11, 29	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∧ (1.‘𝐾)) = (𝑅 ∨ 𝑆))
31	21, 26, 30	3eqtrrd 2771	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∨ 𝑆) = (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ 𝑅))
32	31	oveq1d 7361	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∨ 𝑇) = ((((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ 𝑅) ∨ 𝑇))
33		simp22r 1294	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑆 ≤ 𝑊)
34		simp3r 1203	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
35		simp3l 1202	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))
36		eqid 2731	. . . . . . . 8 ⊢ ((𝑅 ∨ 𝑆) ∧ 𝑊) = ((𝑅 ∨ 𝑆) ∧ 𝑊)
37	16, 8, 19, 9, 13, 36	cdlemeda 40343	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐴)
38	4, 12, 6, 33, 5, 34, 35, 37	syl223anc 1398	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐴)
39		simp23 1209	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑇 ∈ 𝐴)
40	8, 9	hlatjass 39415	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → ((((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ 𝑅) ∨ 𝑇) = (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ (𝑅 ∨ 𝑇)))
41	4, 38, 5, 39, 40	syl13anc 1374	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ 𝑅) ∨ 𝑇) = (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ (𝑅 ∨ 𝑇)))
42	32, 41	eqtrd 2766	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∨ 𝑇) = (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ (𝑅 ∨ 𝑇)))
43	42	oveq1d 7361	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (((𝑅 ∨ 𝑆) ∨ 𝑇) ∧ 𝑊) = ((((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ (𝑅 ∨ 𝑇)) ∧ 𝑊))
44	7, 8, 9	hlatjcl 39412	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑅 ∨ 𝑇) ∈ (Base‘𝐾))
45	4, 5, 39, 44	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∨ 𝑇) ∈ (Base‘𝐾))
46	4	hllatd 39409	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ Lat)
47	7, 16, 19	latmle2 18371	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊)
48	46, 11, 15, 47	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊)
49	7, 16, 8, 19, 9	atmod1i1 39902	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐴 ∧ (𝑅 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ ((𝑅 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊) → (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ ((𝑅 ∨ 𝑇) ∧ 𝑊)) = ((((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ (𝑅 ∨ 𝑇)) ∧ 𝑊))
50	4, 38, 45, 15, 48, 49	syl131anc 1385	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ ((𝑅 ∨ 𝑇) ∧ 𝑊)) = ((((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ (𝑅 ∨ 𝑇)) ∧ 𝑊))
51	43, 50	eqtr4d 2769	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (((𝑅 ∨ 𝑆) ∨ 𝑇) ∧ 𝑊) = (((𝑅 ∨ 𝑆) ∧ 𝑊) ∨ ((𝑅 ∨ 𝑇) ∧ 𝑊)))
52	3, 51	eqtr4id 2785	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝐷 ∨ 𝑌) = (((𝑅 ∨ 𝑆) ∨ 𝑇) ∧ 𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 class class class wbr 5091 ‘cfv 6481 (class class class)co 7346 Basecbs 17120 lecple 17168 joincjn 18217 meetcmee 18218 1.cp1 18328 Latclat 18337 OLcol 39219 Atomscatm 39308 HLchlt 39395 LHypclh 40029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-id 5511 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-1st 7921 df-2nd 7922 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 39221 df-ol 39223 df-oml 39224 df-covers 39311 df-ats 39312 df-atl 39343 df-cvlat 39367 df-hlat 39396 df-psubsp 39548 df-pmap 39549 df-padd 39841 df-lhyp 40033

This theorem is referenced by: cdleme20d 40357

W3C validator