Theorem cdleme11g 40262

Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 40267. (Contributed by NM, 14-Jun-2012.)

Hypotheses

Ref	Expression
cdleme11.l	⊢ ≤ = (le‘𝐾)
cdleme11.j	⊢ ∨ = (join‘𝐾)
cdleme11.m	⊢ ∧ = (meet‘𝐾)
cdleme11.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme11.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme11.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme11.c	⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
cdleme11.d	⊢ 𝐷 = ((𝑃 ∨ 𝑇) ∧ 𝑊)
cdleme11.f	⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))

Assertion

Ref	Expression
cdleme11g	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ 𝐹) = (𝑄 ∨ 𝐶))

Proof of Theorem cdleme11g

Step	Hyp	Ref	Expression
1		cdleme11.f	. . . 4 ⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
2	1	oveq2i 7449	. . 3 ⊢ (𝑄 ∨ 𝐹) = (𝑄 ∨ ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
3		simp1l 1198	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝐾 ∈ HL)
4		simp22l 1293	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑄 ∈ 𝐴)
5	3	hllatd 39360	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝐾 ∈ Lat)
6		simp23 1209	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑆 ∈ 𝐴)
7		eqid 2737	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
8		cdleme11.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
9	7, 8	atbase 39285	. . . . . 6 ⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾))
10	6, 9	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑆 ∈ (Base‘𝐾))
11		simp1 1137	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		simp21 1207	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝐴)
13		cdleme11.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
14		cdleme11.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
15		cdleme11.m	. . . . . . 7 ⊢ ∧ = (meet‘𝐾)
16		cdleme11.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
17		cdleme11.u	. . . . . . 7 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
18	13, 14, 15, 8, 16, 17, 7	cdleme0aa 40207	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑈 ∈ (Base‘𝐾))
19	11, 12, 4, 18	syl3anc 1372	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑈 ∈ (Base‘𝐾))
20	7, 14	latjcl 18506	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (𝑆 ∨ 𝑈) ∈ (Base‘𝐾))
21	5, 10, 19, 20	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑆 ∨ 𝑈) ∈ (Base‘𝐾))
22	7, 8	atbase 39285	. . . . . 6 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
23	4, 22	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑄 ∈ (Base‘𝐾))
24	7, 8	atbase 39285	. . . . . . . 8 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
25	12, 24	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ (Base‘𝐾))
26	7, 14	latjcl 18506	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
27	5, 25, 10, 26	syl3anc 1372	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
28		simp1r 1199	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑊 ∈ 𝐻)
29	7, 16	lhpbase 39995	. . . . . . 7 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑊 ∈ (Base‘𝐾))
31	7, 15	latmcl 18507	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾))
32	5, 27, 30, 31	syl3anc 1372	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾))
33	7, 14	latjcl 18506	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾)) → (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ∈ (Base‘𝐾))
34	5, 23, 32, 33	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ∈ (Base‘𝐾))
35	7, 13, 14	latlej1 18515	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾)) → 𝑄 ≤ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
36	5, 23, 32, 35	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝑄 ≤ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
37	7, 13, 14, 15, 8	atmod1i1 39854	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ (𝑆 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑄 ≤ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) → (𝑄 ∨ ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))) = ((𝑄 ∨ (𝑆 ∨ 𝑈)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
38	3, 4, 21, 34, 36, 37	syl131anc 1384	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))) = ((𝑄 ∨ (𝑆 ∨ 𝑈)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
39	2, 38	eqtrid 2789	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ 𝐹) = ((𝑄 ∨ (𝑆 ∨ 𝑈)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
40		simp22 1208	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
41	13, 14, 15, 8, 16, 17	cdleme0cq 40212	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝑄 ∨ 𝑈) = (𝑃 ∨ 𝑄))
42	11, 12, 40, 41	syl12anc 837	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ 𝑈) = (𝑃 ∨ 𝑄))
43	42	oveq2d 7454	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑆 ∨ (𝑄 ∨ 𝑈)) = (𝑆 ∨ (𝑃 ∨ 𝑄)))
44	7, 14	latj12 18551	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → (𝑄 ∨ (𝑆 ∨ 𝑈)) = (𝑆 ∨ (𝑄 ∨ 𝑈)))
45	5, 23, 10, 19, 44	syl13anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ (𝑆 ∨ 𝑈)) = (𝑆 ∨ (𝑄 ∨ 𝑈)))
46	7, 14	latj13 18553	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (𝑄 ∨ (𝑃 ∨ 𝑆)) = (𝑆 ∨ (𝑃 ∨ 𝑄)))
47	5, 23, 25, 10, 46	syl13anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ (𝑃 ∨ 𝑆)) = (𝑆 ∨ (𝑃 ∨ 𝑄)))
48	43, 45, 47	3eqtr4d 2787	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ (𝑆 ∨ 𝑈)) = (𝑄 ∨ (𝑃 ∨ 𝑆)))
49	48	oveq1d 7453	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑄 ∨ (𝑆 ∨ 𝑈)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) = ((𝑄 ∨ (𝑃 ∨ 𝑆)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
50	7, 13, 15	latmle1 18531	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ (𝑃 ∨ 𝑆))
51	5, 27, 30, 50	syl3anc 1372	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ (𝑃 ∨ 𝑆))
52	7, 13, 14	latjlej2 18521	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((𝑃 ∨ 𝑆) ∧ 𝑊) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ (𝑃 ∨ 𝑆) → (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑃 ∨ 𝑆))))
53	5, 32, 27, 23, 52	syl13anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ (𝑃 ∨ 𝑆) → (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑃 ∨ 𝑆))))
54	51, 53	mpd 15	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑃 ∨ 𝑆)))
55	7, 14	latjcl 18506	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → (𝑄 ∨ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
56	5, 23, 27, 55	syl3anc 1372	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾))
57	7, 13, 15	latleeqm2 18535	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ∈ (Base‘𝐾) ∧ (𝑄 ∨ (𝑃 ∨ 𝑆)) ∈ (Base‘𝐾)) → ((𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑃 ∨ 𝑆)) ↔ ((𝑄 ∨ (𝑃 ∨ 𝑆)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) = (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
58	5, 34, 56, 57	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑃 ∨ 𝑆)) ↔ ((𝑄 ∨ (𝑃 ∨ 𝑆)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) = (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))))
59	54, 58	mpbid 232	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑄 ∨ (𝑃 ∨ 𝑆)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) = (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
60		cdleme11.c	. . . 4 ⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
61	60	oveq2i 7449	. . 3 ⊢ (𝑄 ∨ 𝐶) = (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))
62	59, 61	eqtr4di 2795	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑄 ∨ (𝑃 ∨ 𝑆)) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) = (𝑄 ∨ 𝐶))
63	39, 49, 62	3eqtrd 2781	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑄 ∨ 𝐹) = (𝑄 ∨ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1539   ∈ wcel 2108   ≠ wne 2940   class class class wbr 5151  ‘cfv 6569  (class class class)co 7438  Basecbs 17254  lecple 17314  joincjn 18378  meetcmee 18379  Latclat 18498  Atomscatm 39259  HLchlt 39346  LHypclh 39981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5288  ax-sep 5305  ax-nul 5315  ax-pow 5374  ax-pr 5441  ax-un 7761

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3483  df-sbc 3795  df-csb 3912  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-iun 5001  df-iin 5002  df-br 5152  df-opab 5214  df-mpt 5235  df-id 5587  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576  df-fv 6577  df-riota 7395  df-ov 7441  df-oprab 7442  df-mpo 7443  df-1st 8022  df-2nd 8023  df-proset 18361  df-poset 18380  df-plt 18397  df-lub 18413  df-glb 18414  df-join 18415  df-meet 18416  df-p0 18492  df-p1 18493  df-lat 18499  df-clat 18566  df-oposet 39172  df-ol 39174  df-oml 39175  df-covers 39262  df-ats 39263  df-atl 39294  df-cvlat 39318  df-hlat 39347  df-psubsp 39500  df-pmap 39501  df-padd 39793  df-lhyp 39985

This theorem is referenced by:  cdleme11h  40263  cdleme11j  40264  cdleme15a  40271