Metamath Proof Explorer

Theorem fuco23

Description: The morphism part of the functor composition bifunctor. See also fuco23a . (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses fuco22.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
fuco22.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
fuco22.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
fuco22.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
fuco22.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
fuco23.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
fuco23.o ⊢ ( 𝜑 → ∗ = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
Assertion fuco23 ( 𝜑 → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ∗ ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 fuco22.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2 fuco22.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
3 fuco22.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
4 fuco22.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
5 fuco22.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
6 fuco23.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
7 fuco23.o ⊢ ( 𝜑 → ∗ = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
8 1 2 3 4 5 fuco22 ⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
10 9 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
11 10 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) )
12 9 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑋 ) )
13 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) = ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) )
14 11 13 opeq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ = ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ )
15 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) = ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) )
16 14 15 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ∗ = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
18 16 17 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ∗ )
19 12 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) = ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) )
20 10 12 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) )
21 9 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
22 20 21 fveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) )
23 18 19 22 oveq123d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ∗ ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
24 ovexd ⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ∗ ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ∈ V )
25 8 23 6 24 fvmptd ⊢ ( 𝜑 → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ∗ ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )