Metamath Proof Explorer

Theorem upciclem3

Description: Lemma for upciclem4 . (Contributed by Zhi Wang, 17-Sep-2025)

Ref Expression
Hypotheses upcic.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
upcic.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
upcic.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
upcic.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
upcic.o ⊢ 𝑂 = ( comp ‘ 𝐸 )
upcic.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
upcic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
upcic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
upcic.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
upcic.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
upcic.1 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
upciclem3.od ⊢ · = ( comp ‘ 𝐷 )
upciclem3.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
upciclem3.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 𝐻 𝑋 ) )
upciclem3.mn ⊢ ( 𝜑 → 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝐿 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
upciclem3.nm ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
Assertion upciclem3 ( 𝜑 → ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 upcic.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 upcic.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
3 upcic.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
4 upcic.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
5 upcic.o ⊢ 𝑂 = ( comp ‘ 𝐸 )
6 upcic.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
7 upcic.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 upcic.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 upcic.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
10 upcic.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
11 upcic.1 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
12 upciclem3.od ⊢ · = ( comp ‘ 𝐷 )
13 upciclem3.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
14 upciclem3.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 𝐻 𝑋 ) )
15 upciclem3.mn ⊢ ( 𝜑 → 𝑀 = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝐿 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
16 upciclem3.nm ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
17 fveq2 ⊢ ( 𝑝 = ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) = ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ) )
18 17 oveq1d ⊢ ( 𝑝 = ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) → ( ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) )
19 18 eqeq2d ⊢ ( 𝑝 = ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) → ( 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) ↔ 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) ) )
20 fveq2 ⊢ ( 𝑝 = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) → ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) = ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) )
21 20 oveq1d ⊢ ( 𝑝 = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) → ( ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) )
22 21 eqeq2d ⊢ ( 𝑝 = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) → ( 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) ↔ 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) ) )
23 11 7 10 upciclem1 ⊢ ( 𝜑 → ∃! 𝑝 ∈ ( 𝑋 𝐻 𝑋 ) 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ 𝑝 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) )
24 6 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
25 1 3 12 24 7 8 7 13 14 catcocl ⊢ ( 𝜑 → ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ∈ ( 𝑋 𝐻 𝑋 ) )
26 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
27 1 3 26 24 7 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
28 1 2 3 4 5 6 7 8 7 9 10 12 13 14 16 upciclem2 ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝐿 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑁 ) )
29 15 28 eqtr4d ⊢ ( 𝜑 → 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) )
30 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
31 1 26 30 6 7 funcid ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
32 31 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) = ( ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) )
33 6 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
34 1 2 6 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
35 34 7 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐶 )
36 2 4 30 33 9 5 35 10 catlid ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) = 𝑀 )
37 32 36 eqtr2d ⊢ ( 𝜑 → 𝑀 = ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑋 ) ) 𝑀 ) )
38 19 22 23 25 27 29 37 reu2eqd ⊢ ( 𝜑 → ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑋 ) 𝐾 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) )