Theorem cdlemk55u 40571

Description: Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. 𝐺, 𝐼 stand for g, h. 𝑋 represents tau. (Contributed by NM, 31-Jul-2013.)

Hypotheses

Ref	Expression
cdlemk5.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk5.l	⊢ ≤ = (le‘𝐾)
cdlemk5.j	⊢ ∨ = (join‘𝐾)
cdlemk5.m	⊢ ∧ = (meet‘𝐾)
cdlemk5.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk5.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk5.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk5.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk5.z	⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))))
cdlemk5.y	⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏))))
cdlemk5.x	⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌))
cdlemk5.u	⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋))

Assertion

Ref	Expression
cdlemk55u	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘(𝐺 ∘ 𝐼)) = ((𝑈‘𝐺) ∘ (𝑈‘𝐼)))

Distinct variable groups:   ∧ ,𝑔   ∨ ,𝑔   𝐵,𝑔   𝑃,𝑔   𝑅,𝑔   𝑇,𝑔   𝑔,𝑍   𝑔,𝑏,𝐺,𝑧   ∧ ,𝑏,𝑧   ≤ ,𝑏   𝑧,𝑔, ≤   ∨ ,𝑏,𝑧   𝐴,𝑏,𝑔,𝑧   𝐵,𝑏,𝑧   𝐹,𝑏,𝑔,𝑧   𝑧,𝐺   𝐻,𝑏,𝑔,𝑧   𝐾,𝑏,𝑔,𝑧   𝑁,𝑏,𝑔,𝑧   𝑃,𝑏,𝑧   𝑅,𝑏,𝑧   𝑇,𝑏,𝑧   𝑊,𝑏,𝑔,𝑧   𝑧,𝑌   𝐺,𝑏   𝐼,𝑏,𝑔,𝑧

Allowed substitution hints:   𝑈(𝑧,𝑔,𝑏)   𝑋(𝑧,𝑔,𝑏)   𝑌(𝑔,𝑏)   𝑍(𝑧,𝑏)

Proof of Theorem cdlemk55u

Step	Hyp	Ref	Expression
1		simpr 483	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → 𝐹 = 𝑁)
2		simp11 1200	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3		simp22 1204	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
4		simp23 1205	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐼 ∈ 𝑇)
5		cdlemk5.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
6		cdlemk5.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
7	5, 6	ltrnco 40324	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) → (𝐺 ∘ 𝐼) ∈ 𝑇)
8	2, 3, 4, 7	syl3anc 1368	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ 𝐼) ∈ 𝑇)
9	8	adantr 479	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝐺 ∘ 𝐼) ∈ 𝑇)
10		cdlemk5.x	. . . . 5 ⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌))
11		cdlemk5.u	. . . . 5 ⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋))
12	10, 11	cdlemk40t 40523	. . . 4 ⊢ ((𝐹 = 𝑁 ∧ (𝐺 ∘ 𝐼) ∈ 𝑇) → (𝑈‘(𝐺 ∘ 𝐼)) = (𝐺 ∘ 𝐼))
13	1, 9, 12	syl2anc 582	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝑈‘(𝐺 ∘ 𝐼)) = (𝐺 ∘ 𝐼))
14		simpl22 1249	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → 𝐺 ∈ 𝑇)
15	10, 11	cdlemk40t 40523	. . . . 5 ⊢ ((𝐹 = 𝑁 ∧ 𝐺 ∈ 𝑇) → (𝑈‘𝐺) = 𝐺)
16	1, 14, 15	syl2anc 582	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝑈‘𝐺) = 𝐺)
17		simpl23 1250	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → 𝐼 ∈ 𝑇)
18	10, 11	cdlemk40t 40523	. . . . 5 ⊢ ((𝐹 = 𝑁 ∧ 𝐼 ∈ 𝑇) → (𝑈‘𝐼) = 𝐼)
19	1, 17, 18	syl2anc 582	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝑈‘𝐼) = 𝐼)
20	16, 19	coeq12d 5867	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → ((𝑈‘𝐺) ∘ (𝑈‘𝐼)) = (𝐺 ∘ 𝐼))
21	13, 20	eqtr4d 2768	. 2 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝑈‘(𝐺 ∘ 𝐼)) = ((𝑈‘𝐺) ∘ (𝑈‘𝐼)))
22		simpl1 1188	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇))
23		simpl21 1248	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → (𝑅‘𝐹) = (𝑅‘𝑁))
24		simpr 483	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → 𝐹 ≠ 𝑁)
25	23, 24	jca 510	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁))
26		simpl22 1249	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → 𝐺 ∈ 𝑇)
27		simpl23 1250	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → 𝐼 ∈ 𝑇)
28		simpl3 1190	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
29		cdlemk5.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
30		cdlemk5.l	. . . 4 ⊢ ≤ = (le‘𝐾)
31		cdlemk5.j	. . . 4 ⊢ ∨ = (join‘𝐾)
32		cdlemk5.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
33		cdlemk5.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
34		cdlemk5.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
35		cdlemk5.z	. . . 4 ⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))))
36		cdlemk5.y	. . . 4 ⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏))))
37	29, 30, 31, 32, 33, 5, 6, 34, 35, 36, 10, 11	cdlemk55u1 40570	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐹 ≠ 𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘(𝐺 ∘ 𝐼)) = ((𝑈‘𝐺) ∘ (𝑈‘𝐼)))
38	22, 25, 26, 27, 28, 37	syl131anc 1380	. 2 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → (𝑈‘(𝐺 ∘ 𝐼)) = ((𝑈‘𝐺) ∘ (𝑈‘𝐼)))
39	21, 38	pm2.61dane 3018	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ ((𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘(𝐺 ∘ 𝐼)) = ((𝑈‘𝐺) ∘ (𝑈‘𝐼)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  ∀wral 3050  ifcif 4530   class class class wbr 5149   ↦ cmpt 5232   I cid 5575  ^◡ccnv 5677   ↾ cres 5680   ∘ ccom 5682  ‘cfv 6549  ℩crio 7374  (class class class)co 7419  Basecbs 17188  lecple 17248  joincjn 18311  meetcmee 18312  Atomscatm 38867  HLchlt 38954  LHypclh 39589  LTrncltrn 39706  trLctrl 39763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-riotaBAD 38557

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-undef 8279  df-map 8847  df-proset 18295  df-poset 18313  df-plt 18330  df-lub 18346  df-glb 18347  df-join 18348  df-meet 18349  df-p0 18425  df-p1 18426  df-lat 18432  df-clat 18499  df-oposet 38780  df-ol 38782  df-oml 38783  df-covers 38870  df-ats 38871  df-atl 38902  df-cvlat 38926  df-hlat 38955  df-llines 39103  df-lplanes 39104  df-lvols 39105  df-lines 39106  df-psubsp 39108  df-pmap 39109  df-padd 39401  df-lhyp 39593  df-laut 39594  df-ldil 39709  df-ltrn 39710  df-trl 39764

This theorem is referenced by:  cdlemk56  40576