Theorem cdlemi2 37982

Description: Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)

Hypotheses

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

Assertion

Ref	Expression
cdlemi2	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))

Proof of Theorem cdlemi2

Step	Hyp	Ref	Expression
1		simp1l 1193	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
2		simp1r 1194	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
3		simp21 1202	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑈 ∈ 𝐸)
4		simp1 1132	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
5		simp23 1204	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
6		simp22 1203	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
7		cdlemi.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
8		cdlemi.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9	7, 8	ltrncnv 37309	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇)
10	4, 6, 9	syl2anc 586	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇)
11	7, 8	ltrnco 37882	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝐺 ∘ ◡𝐹) ∈ 𝑇)
12	4, 5, 10, 11	syl3anc 1367	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ◡𝐹) ∈ 𝑇)
13		cdlemi.e	. . . . . . 7 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
14	7, 8, 13	tendovalco 37928	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑈 ∈ 𝐸) ∧ ((𝐺 ∘ ◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇)) → (𝑈‘((𝐺 ∘ ◡𝐹) ∘ 𝐹)) = ((𝑈‘(𝐺 ∘ ◡𝐹)) ∘ (𝑈‘𝐹)))
15	1, 2, 3, 12, 6, 14	syl32anc 1374	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘((𝐺 ∘ ◡𝐹) ∘ 𝐹)) = ((𝑈‘(𝐺 ∘ ◡𝐹)) ∘ (𝑈‘𝐹)))
16		coass 6099	. . . . . . 7 ⊢ ((𝐺 ∘ ◡𝐹) ∘ 𝐹) = (𝐺 ∘ (◡𝐹 ∘ 𝐹))
17		cdlemi.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐾)
18	17, 7, 8	ltrn1o 37287	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
19	4, 6, 18	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:𝐵–1-1-onto→𝐵)
20		f1ococnv1 6624	. . . . . . . . . 10 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵))
22	21	coeq2d 5714	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (◡𝐹 ∘ 𝐹)) = (𝐺 ∘ ( I ↾ 𝐵)))
23	17, 7, 8	ltrn1o 37287	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺:𝐵–1-1-onto→𝐵)
24	4, 5, 23	syl2anc 586	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺:𝐵–1-1-onto→𝐵)
25		f1of 6596	. . . . . . . . 9 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵⟶𝐵)
26		fcoi1 6533	. . . . . . . . 9 ⊢ (𝐺:𝐵⟶𝐵 → (𝐺 ∘ ( I ↾ 𝐵)) = 𝐺)
27	24, 25, 26	3syl 18	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ( I ↾ 𝐵)) = 𝐺)
28	22, 27	eqtrd 2855	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ (◡𝐹 ∘ 𝐹)) = 𝐺)
29	16, 28	syl5eq 2867	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺 ∘ ◡𝐹) ∘ 𝐹) = 𝐺)
30	29	fveq2d 6655	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘((𝐺 ∘ ◡𝐹) ∘ 𝐹)) = (𝑈‘𝐺))
31	15, 30	eqtr3d 2857	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘(𝐺 ∘ ◡𝐹)) ∘ (𝑈‘𝐹)) = (𝑈‘𝐺))
32	31	fveq1d 6653	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑈‘(𝐺 ∘ ◡𝐹)) ∘ (𝑈‘𝐹))‘𝑃) = ((𝑈‘𝐺)‘𝑃))
33	7, 8, 13	tendocl 37930	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ (𝐺 ∘ ◡𝐹) ∈ 𝑇) → (𝑈‘(𝐺 ∘ ◡𝐹)) ∈ 𝑇)
34	4, 3, 12, 33	syl3anc 1367	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘(𝐺 ∘ ◡𝐹)) ∈ 𝑇)
35	7, 8, 13	tendocl 37930	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑈‘𝐹) ∈ 𝑇)
36	4, 3, 6, 35	syl3anc 1367	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐹) ∈ 𝑇)
37		simp3l 1197	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
38		cdlemi.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
39		cdlemi.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
40	38, 39, 7, 8	ltrncoval 37308	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑈‘(𝐺 ∘ ◡𝐹)) ∈ 𝑇 ∧ (𝑈‘𝐹) ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝑈‘(𝐺 ∘ ◡𝐹)) ∘ (𝑈‘𝐹))‘𝑃) = ((𝑈‘(𝐺 ∘ ◡𝐹))‘((𝑈‘𝐹)‘𝑃)))
41	4, 34, 36, 37, 40	syl121anc 1371	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑈‘(𝐺 ∘ ◡𝐹)) ∘ (𝑈‘𝐹))‘𝑃) = ((𝑈‘(𝐺 ∘ ◡𝐹))‘((𝑈‘𝐹)‘𝑃)))
42	32, 41	eqtr3d 2857	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) = ((𝑈‘(𝐺 ∘ ◡𝐹))‘((𝑈‘𝐹)‘𝑃)))
43	38, 39, 7, 8	ltrnel 37302	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐹) ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊))
44	36, 43	syld3an2 1407	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊))
45		cdlemi.j	. . . 4 ⊢ ∨ = (join‘𝐾)
46		cdlemi.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
47		cdlemi.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
48	17, 38, 45, 46, 39, 7, 8, 47, 13	cdlemi1 37981	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ (𝐺 ∘ ◡𝐹) ∈ 𝑇) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊)) → ((𝑈‘(𝐺 ∘ ◡𝐹))‘((𝑈‘𝐹)‘𝑃)) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))
49	4, 3, 12, 44, 48	syl121anc 1371	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘(𝐺 ∘ ◡𝐹))‘((𝑈‘𝐹)‘𝑃)) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))
50	42, 49	eqbrtrd 5069	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   class class class wbr 5047   I cid 5440  ^◡ccnv 5535   ↾ cres 5538   ∘ ccom 5540  ⟶wf 6332  –1-1-onto→wf1o 6335  ‘cfv 6336  (class class class)co 7137  Basecbs 16461  lecple 16550  joincjn 17532  meetcmee 17533  Atomscatm 36426  HLchlt 36513  LHypclh 37147  LTrncltrn 37264  trLctrl 37321  TEndoctendo 37915

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7442  ax-riotaBAD 36116

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3012  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3483  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-iin 4903  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7095  df-ov 7140  df-oprab 7141  df-mpo 7142  df-1st 7670  df-2nd 7671  df-undef 7920  df-map 8389  df-proset 17516  df-poset 17534  df-plt 17546  df-lub 17562  df-glb 17563  df-join 17564  df-meet 17565  df-p0 17627  df-p1 17628  df-lat 17634  df-clat 17696  df-oposet 36339  df-ol 36341  df-oml 36342  df-covers 36429  df-ats 36430  df-atl 36461  df-cvlat 36485  df-hlat 36514  df-llines 36661  df-lplanes 36662  df-lvols 36663  df-lines 36664  df-psubsp 36666  df-pmap 36667  df-padd 36959  df-lhyp 37151  df-laut 37152  df-ldil 37267  df-ltrn 37268  df-trl 37322  df-tendo 37918

This theorem is referenced by:  cdlemi  37983