cdlemk4 - Mathbox for Norm Megill

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

Theorem cdlemk4 40831

Description: Part of proof of Lemma K of [Crawley] p. 118, last line. We use 𝑋 for their h, since 𝐻 is already used. (Contributed by NM, 24-Jun-2013.)

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

**Assertion**
Ref	Expression
cdlemk4	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))

**Proof of Theorem cdlemk4**
Step	Hyp	Ref	Expression
1		simp1l 1198	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
2		simp1 1137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp2l 1200	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
4		simp3l 1202	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
5		cdlemk.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
6		cdlemk.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
7		cdlemk.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
8		cdlemk.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9	5, 6, 7, 8	ltrnat 40137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)
10	2, 3, 4, 9	syl3anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴)
11		simp2r 1201	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇)
12	5, 6, 7, 8	ltrnat 40137	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐴)
13	2, 11, 4, 12	syl3anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐴)
14		cdlemk.j	. . . 4 ⊢ ∨ = (join‘𝐾)
15	5, 14, 6	hlatlej1 39371	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
16	1, 10, 13, 15	syl3anc 1372	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
17	1	hllatd 39360	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
18		cdlemk.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
19	18, 6	atbase 39285	. . . . . 6 ⊢ ((𝐹‘𝑃) ∈ 𝐴 → (𝐹‘𝑃) ∈ 𝐵)
20	10, 19	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐵)
21	18, 6	atbase 39285	. . . . . 6 ⊢ ((𝑋‘𝑃) ∈ 𝐴 → (𝑋‘𝑃) ∈ 𝐵)
22	13, 21	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐵)
23	18, 14	latjcl 18506	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑃) ∈ 𝐵 ∧ (𝑋‘𝑃) ∈ 𝐵) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
24	17, 20, 22, 23	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
25		simp1r 1199	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
26	18, 7	lhpbase 39995	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
27	25, 26	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵)
28	5, 14, 6	hlatlej2 39372	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
29	1, 10, 13, 28	syl3anc 1372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
30		cdlemk.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
31	18, 5, 14, 30, 6	atmod3i1 39861	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑋‘𝑃) ∈ 𝐴 ∧ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) → ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)))
32	1, 13, 24, 27, 29, 31	syl131anc 1384	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)))
33	7, 8	ltrncnv 40143	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
34	2, 3, 33	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ^◡𝐹 ∈ 𝑇)
35	7, 8	ltrnco 40716	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
36	2, 11, 34, 35	syl3anc 1372	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
37	5, 6, 7, 8	ltrnel 40136	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
38	3, 37	syld3an2 1412	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
39		cdlemk.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
40	5, 14, 30, 6, 7, 8, 39	trlval2 40160	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐹) ∈ 𝑇 ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊))
41	2, 36, 38, 40	syl3anc 1372	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊))
42	18, 7, 8	ltrn1o 40121	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
43	2, 3, 42	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:𝐵–1-1-onto→𝐵)
44		f1ococnv1 6885	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
45	43, 44	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
46	45	coeq2d 5880	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ (^◡𝐹 ∘ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐵)))
47	18, 7, 8	ltrn1o 40121	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇) → 𝑋:𝐵–1-1-onto→𝐵)
48	2, 11, 47	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋:𝐵–1-1-onto→𝐵)
49		f1of 6856	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐵–1-1-onto→𝐵 → 𝑋:𝐵⟶𝐵)
50		fcoi1 6790	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐵⟶𝐵 → (𝑋 ∘ ( I ↾ 𝐵)) = 𝑋)
51	48, 49, 50	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ( I ↾ 𝐵)) = 𝑋)
52	46, 51	eqtr2d 2778	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 = (𝑋 ∘ (^◡𝐹 ∘ 𝐹)))
53		coass 6293	. . . . . . . . . . 11 ⊢ ((𝑋 ∘ ^◡𝐹) ∘ 𝐹) = (𝑋 ∘ (^◡𝐹 ∘ 𝐹))
54	52, 53	eqtr4di 2795	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 = ((𝑋 ∘ ^◡𝐹) ∘ 𝐹))
55	54	fveq1d 6916	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) = (((𝑋 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃))
56	5, 6, 7, 8	ltrncoval 40142	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∘ ^◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝑋 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
57	2, 36, 3, 4, 56	syl121anc 1376	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑋 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
58	55, 57	eqtrd 2777	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) = ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
59	58	oveq2d 7454	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = ((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))))
60	59	eqcomd 2743	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
61	60	oveq1d 7453	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))
62	41, 61	eqtrd 2777	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))
63	62	oveq2d 7454	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) = ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)))
64	5, 6, 7, 8	ltrnel 40136	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊))
65	11, 64	syld3an2 1412	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊))
66		eqid 2737	. . . . . . 7 ⊢ (1.‘𝐾) = (1.‘𝐾)
67	5, 14, 66, 6, 7	lhpjat2 40018	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊)) → ((𝑋‘𝑃) ∨ 𝑊) = (1.‘𝐾))
68	2, 65, 67	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ 𝑊) = (1.‘𝐾))
69	68	oveq2d 7454	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)))
70		hlol 39357	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
71	1, 70	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ OL)
72	18, 30, 66	olm11 39223	. . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
73	71, 24, 72	syl2anc 584	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
74	69, 73	eqtr2d 2778	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)))
75	32, 63, 74	3eqtr4rd 2788	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))
76	16, 75	breqtrd 5177	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1539 ∈ wcel 2108 class class class wbr 5151 I cid 5586 ^◡ccnv 5692 ↾ cres 5695 ∘ ccom 5697 ⟶wf 6565 –1-1-onto→wf1o 6568 ‘cfv 6569 (class class class)co 7438 Basecbs 17254 lecple 17314 joincjn 18378 meetcmee 18379 1.cp1 18491 Latclat 18498 OLcol 39170 Atomscatm 39259 HLchlt 39346 LHypclh 39981 LTrncltrn 40098 trLctrl 40155

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 ax-riotaBAD 38949

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 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-undef 8306 df-map 8876 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-llines 39495 df-lplanes 39496 df-lvols 39497 df-lines 39498 df-psubsp 39500 df-pmap 39501 df-padd 39793 df-lhyp 39985 df-laut 39986 df-ldil 40101 df-ltrn 40102 df-trl 40156

This theorem is referenced by: cdlemk5a 40832

W3C validator