Metamath Proof Explorer

Theorem upciclem2

Description: Lemma for upciclem3 and upeu2 . (Contributed by Zhi Wang, 19-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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
upciclem2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
upciclem2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
upciclem2.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
upciclem2.od ⊢ · = ( comp ‘ 𝐷 )
upciclem2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
upciclem2.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 𝐻 𝑍 ) )
upciclem2.nm ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
Assertion upciclem2 ( 𝜑 → ( ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐾 ) ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑀 ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑁 ) )

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 upciclem2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10 upciclem2.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
11 upciclem2.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑊 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
12 upciclem2.od ⊢ · = ( comp ‘ 𝐷 )
13 upciclem2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
14 upciclem2.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 𝐻 𝑍 ) )
15 upciclem2.nm ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
16 6 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
17 1 2 6 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
18 17 7 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐶 )
19 17 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ 𝐶 )
20 1 3 4 6 7 8 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
21 20 13 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
22 17 9 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑍 ) ∈ 𝐶 )
23 1 3 4 6 8 9 funcf2 ⊢ ( 𝜑 → ( 𝑌 𝐺 𝑍 ) : ( 𝑌 𝐻 𝑍 ) ⟶ ( ( 𝐹 ‘ 𝑌 ) 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
24 23 14 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ∈ ( ( 𝐹 ‘ 𝑌 ) 𝐽 ( 𝐹 ‘ 𝑍 ) ) )
25 2 4 5 16 10 18 19 11 21 22 24 catass ⊢ ( 𝜑 → ( ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑀 ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
26 1 3 12 5 6 7 8 9 13 14 funcco ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐾 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ) )
27 26 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐾 ) ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑀 ) = ( ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑀 ) )
28 15 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑁 ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
29 25 27 28 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐾 ) ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑀 ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐿 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑍 ) ) 𝑁 ) )