Theorem cdlemc6 40644

Description: Lemma for cdlemc 40645. (Contributed by NM, 26-May-2012.)

Hypotheses

Ref	Expression
cdlemc3.l	⊢ ≤ = (le‘𝐾)
cdlemc3.j	⊢ ∨ = (join‘𝐾)
cdlemc3.m	⊢ ∧ = (meet‘𝐾)
cdlemc3.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemc3.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemc3.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemc3.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

Assertion

Ref	Expression
cdlemc6	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑄) = ((𝑄 ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))))

Proof of Theorem cdlemc6

Step	Hyp	Ref	Expression
1		simp1l 1199	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝐾 ∈ HL)
2		simp22l 1294	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑃 ∈ 𝐴)
3		simp23l 1296	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑄 ∈ 𝐴)
4		cdlemc3.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
5		cdlemc3.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
6	4, 5	hlatjcom 39816	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
7	1, 2, 3, 6	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
8	7	oveq2d 7385	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∧ (𝑃 ∨ 𝑄)) = (𝑄 ∧ (𝑄 ∨ 𝑃)))
9	1	hllatd 39812	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝐾 ∈ Lat)
10		eqid 2737	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
11	10, 5	atbase 39737	. . . . 5 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
12	3, 11	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑄 ∈ (Base‘𝐾))
13	10, 5	atbase 39737	. . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
14	2, 13	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑃 ∈ (Base‘𝐾))
15		cdlemc3.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
16	10, 4, 15	latabs2 18444	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑄 ∧ (𝑄 ∨ 𝑃)) = 𝑄)
17	9, 12, 14, 16	syl3anc 1374	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∧ (𝑄 ∨ 𝑃)) = 𝑄)
18	8, 17	eqtrd 2772	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∧ (𝑃 ∨ 𝑄)) = 𝑄)
19		simp1 1137	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
20		simp22 1209	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
21		simp21 1208	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝐹 ∈ 𝑇)
22		simp3 1139	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑃) = 𝑃)
23		cdlemc3.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
24		eqid 2737	. . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾)
25		cdlemc3.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
26		cdlemc3.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
27		cdlemc3.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
28	23, 24, 5, 25, 26, 27	trl0 40618	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑅‘𝐹) = (0.‘𝐾))
29	19, 20, 21, 22, 28	syl112anc 1377	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑅‘𝐹) = (0.‘𝐾))
30	29	oveq2d 7385	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ (𝑅‘𝐹)) = (𝑄 ∨ (0.‘𝐾)))
31		hlol 39809	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
32	1, 31	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝐾 ∈ OL)
33	10, 4, 24	olj01 39673	. . . . 5 ⊢ ((𝐾 ∈ OL ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑄 ∨ (0.‘𝐾)) = 𝑄)
34	32, 12, 33	syl2anc 585	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ (0.‘𝐾)) = 𝑄)
35	30, 34	eqtrd 2772	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑄 ∨ (𝑅‘𝐹)) = 𝑄)
36	22	oveq1d 7384	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = (𝑃 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)))
37	10, 4, 5	hlatjcl 39815	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
38	1, 2, 3, 37	syl3anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
39		simp1r 1200	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑊 ∈ 𝐻)
40	10, 25	lhpbase 40446	. . . . . . 7 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
41	39, 40	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑊 ∈ (Base‘𝐾))
42	10, 15	latmcl 18408	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ (Base‘𝐾))
43	9, 38, 41, 42	syl3anc 1374	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ (Base‘𝐾))
44	10, 4	latjcom 18415	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = (((𝑃 ∨ 𝑄) ∧ 𝑊) ∨ 𝑃))
45	9, 14, 43, 44	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑃 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = (((𝑃 ∨ 𝑄) ∧ 𝑊) ∨ 𝑃))
46	23, 4, 5	hlatlej1 39823	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))
47	1, 2, 3, 46	syl3anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → 𝑃 ≤ (𝑃 ∨ 𝑄))
48	10, 23, 4, 15, 5	atmod2i1 40309	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑄)) → (((𝑃 ∨ 𝑄) ∧ 𝑊) ∨ 𝑃) = ((𝑃 ∨ 𝑄) ∧ (𝑊 ∨ 𝑃)))
49	1, 2, 38, 41, 47, 48	syl131anc 1386	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (((𝑃 ∨ 𝑄) ∧ 𝑊) ∨ 𝑃) = ((𝑃 ∨ 𝑄) ∧ (𝑊 ∨ 𝑃)))
50		eqid 2737	. . . . . . . 8 ⊢ (1.‘𝐾) = (1.‘𝐾)
51	23, 4, 50, 5, 25	lhpjat1 40468	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑊 ∨ 𝑃) = (1.‘𝐾))
52	1, 39, 20, 51	syl21anc 838	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝑊 ∨ 𝑃) = (1.‘𝐾))
53	52	oveq2d 7385	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → ((𝑃 ∨ 𝑄) ∧ (𝑊 ∨ 𝑃)) = ((𝑃 ∨ 𝑄) ∧ (1.‘𝐾)))
54	10, 15, 50	olm11 39675	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ (1.‘𝐾)) = (𝑃 ∨ 𝑄))
55	32, 38, 54	syl2anc 585	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → ((𝑃 ∨ 𝑄) ∧ (1.‘𝐾)) = (𝑃 ∨ 𝑄))
56	49, 53, 55	3eqtrd 2776	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (((𝑃 ∨ 𝑄) ∧ 𝑊) ∨ 𝑃) = (𝑃 ∨ 𝑄))
57	36, 45, 56	3eqtrd 2776	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = (𝑃 ∨ 𝑄))
58	35, 57	oveq12d 7387	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → ((𝑄 ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))) = (𝑄 ∧ (𝑃 ∨ 𝑄)))
59	23, 5, 25, 26	ltrnateq 40629	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑄) = 𝑄)
60	18, 58, 59	3eqtr4rd 2783	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹‘𝑃) = 𝑃) → (𝐹‘𝑄) = ((𝑄 ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6500  (class class class)co 7369  Basecbs 17181  lecple 17229  joincjn 18279  meetcmee 18280  0.cp0 18389  1.cp1 18390  Latclat 18399  OLcol 39622  Atomscatm 39711  HLchlt 39798  LHypclh 40432  LTrncltrn 40549  trLctrl 40606

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 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7691

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7944  df-2nd 7945  df-map 8777  df-proset 18262  df-poset 18281  df-plt 18296  df-lub 18312  df-glb 18313  df-join 18314  df-meet 18315  df-p0 18391  df-p1 18392  df-lat 18400  df-clat 18467  df-oposet 39624  df-ol 39626  df-oml 39627  df-covers 39714  df-ats 39715  df-atl 39746  df-cvlat 39770  df-hlat 39799  df-psubsp 39951  df-pmap 39952  df-padd 40244  df-lhyp 40436  df-laut 40437  df-ldil 40552  df-ltrn 40553  df-trl 40607

This theorem is referenced by:  cdlemc  40645