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 41326

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 1204	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
2		simp1 1142	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp2l 1206	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
4		simp3l 1208	. . . 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 40632	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴)
10	2, 3, 4, 9	syl3anc 1379	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴)
11		simp2r 1207	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇)
12	5, 6, 7, 8	ltrnat 40632	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐴)
13	2, 11, 4, 12	syl3anc 1379	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐴)
14		cdlemk.j	. . . 4 ⊢ ∨ = (join‘𝐾)
15	5, 14, 6	hlatlej1 39867	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
16	1, 10, 13, 15	syl3anc 1379	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
17	1	hllatd 39856	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
18		cdlemk.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
19	18, 6	atbase 39781	. . . . . 6 ⊢ ((𝐹‘𝑃) ∈ 𝐴 → (𝐹‘𝑃) ∈ 𝐵)
20	10, 19	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐵)
21	18, 6	atbase 39781	. . . . . 6 ⊢ ((𝑋‘𝑃) ∈ 𝐴 → (𝑋‘𝑃) ∈ 𝐵)
22	13, 21	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐵)
23	18, 14	latjcl 18396	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑃) ∈ 𝐵 ∧ (𝑋‘𝑃) ∈ 𝐵) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
24	17, 20, 22, 23	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)
25		simp1r 1205	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
26	18, 7	lhpbase 40490	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
27	25, 26	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵)
28	5, 14, 6	hlatlej2 39868	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
29	1, 10, 13, 28	syl3anc 1379	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
30		cdlemk.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
31	18, 5, 14, 30, 6	atmod3i1 40356	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑋‘𝑃) ∈ 𝐴 ∧ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) → ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)))
32	1, 13, 24, 27, 29, 31	syl131anc 1391	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)))
33	7, 8	ltrncnv 40638	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
34	2, 3, 33	syl2anc 590	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ^◡𝐹 ∈ 𝑇)
35	7, 8	ltrnco 41211	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
36	2, 11, 34, 35	syl3anc 1379	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ^◡𝐹) ∈ 𝑇)
37	5, 6, 7, 8	ltrnel 40631	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
38	3, 37	syld3an2 1419	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
39		cdlemk.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
40	5, 14, 30, 6, 7, 8, 39	trlval2 40655	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐹) ∈ 𝑇 ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊))
41	2, 36, 38, 40	syl3anc 1379	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊))
42	18, 7, 8	ltrn1o 40616	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
43	2, 3, 42	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:𝐵–1-1-onto→𝐵)
44		f1ococnv1 6796	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
45	43, 44	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
46	45	coeq2d 5804	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ (^◡𝐹 ∘ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐵)))
47	18, 7, 8	ltrn1o 40616	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇) → 𝑋:𝐵–1-1-onto→𝐵)
48	2, 11, 47	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋:𝐵–1-1-onto→𝐵)
49		f1of 6767	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐵–1-1-onto→𝐵 → 𝑋:𝐵⟶𝐵)
50		fcoi1 6701	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐵⟶𝐵 → (𝑋 ∘ ( I ↾ 𝐵)) = 𝑋)
51	48, 49, 50	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ( I ↾ 𝐵)) = 𝑋)
52	46, 51	eqtr2d 2775	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 = (𝑋 ∘ (^◡𝐹 ∘ 𝐹)))
53		coass 6217	. . . . . . . . . . 11 ⊢ ((𝑋 ∘ ^◡𝐹) ∘ 𝐹) = (𝑋 ∘ (^◡𝐹 ∘ 𝐹))
54	52, 53	eqtr4di 2792	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 = ((𝑋 ∘ ^◡𝐹) ∘ 𝐹))
55	54	fveq1d 6829	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) = (((𝑋 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃))
56	5, 6, 7, 8	ltrncoval 40637	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∘ ^◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝑋 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
57	2, 36, 3, 4, 56	syl121anc 1383	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑋 ∘ ^◡𝐹) ∘ 𝐹)‘𝑃) = ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
58	55, 57	eqtrd 2774	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) = ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃)))
59	58	oveq2d 7372	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = ((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))))
60	59	eqcomd 2745	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
61	60	oveq1d 7371	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝑋 ∘ ^◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))
62	41, 61	eqtrd 2774	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ^◡𝐹)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))
63	62	oveq2d 7372	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))) = ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)))
64	5, 6, 7, 8	ltrnel 40631	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊))
65	11, 64	syld3an2 1419	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊))
66		eqid 2739	. . . . . . 7 ⊢ (1.‘𝐾) = (1.‘𝐾)
67	5, 14, 66, 6, 7	lhpjat2 40513	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊)) → ((𝑋‘𝑃) ∨ 𝑊) = (1.‘𝐾))
68	2, 65, 67	syl2anc 590	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ 𝑊) = (1.‘𝐾))
69	68	oveq2d 7372	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)))
70		hlol 39853	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
71	1, 70	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ OL)
72	18, 30, 66	olm11 39719	. . . . 5 ⊢ ((𝐾 ∈ OL ∧ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
73	71, 24, 72	syl2anc 590	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃)))
74	69, 73	eqtr2d 2775	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)))
75	32, 63, 74	3eqtr4rd 2785	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))
76	16, 75	breqtrd 5098	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 class class class wbr 5072 I cid 5512 ^◡ccnv 5617 ↾ cres 5620 ∘ ccom 5622 ⟶wf 6481 –1-1-onto→wf1o 6484 ‘cfv 6485 (class class class)co 7356 Basecbs 17170 lecple 17218 joincjn 18268 meetcmee 18269 1.cp1 18379 Latclat 18388 OLcol 39666 Atomscatm 39755 HLchlt 39842 LHypclh 40476 LTrncltrn 40593 trLctrl 40650

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-riotaBAD 39445

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-1st 7931 df-2nd 7932 df-undef 8213 df-map 8765 df-proset 18251 df-poset 18270 df-plt 18285 df-lub 18301 df-glb 18302 df-join 18303 df-meet 18304 df-p0 18380 df-p1 18381 df-lat 18389 df-clat 18456 df-oposet 39668 df-ol 39670 df-oml 39671 df-covers 39758 df-ats 39759 df-atl 39790 df-cvlat 39814 df-hlat 39843 df-llines 39990 df-lplanes 39991 df-lvols 39992 df-lines 39993 df-psubsp 39995 df-pmap 39996 df-padd 40288 df-lhyp 40480 df-laut 40481 df-ldil 40596 df-ltrn 40597 df-trl 40651

This theorem is referenced by: cdlemk5a 41327

W3C validator