Metamath Proof Explorer

Theorem fuco22

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

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

Proof

Step Hyp Ref Expression
1 fuco22.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2 fuco22.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
3 fuco22.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
4 fuco22.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
5 fuco22.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
6 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
7 6 4 natrcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
8 eqid ⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
9 8 5 natrcl2 ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
10 6 4 natrcl3 ⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
11 8 5 natrcl3 ⊢ ( 𝜑 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
12 1 7 9 2 10 11 3 fuco21 ⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
13 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑏 = 𝐵 )
14 13 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) = ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) )
15 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑎 = 𝐴 )
16 15 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
17 16 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) )
18 14 17 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )
19 18 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) )
20 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ∈ V )
21 20 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) ∈ V )
22 12 19 5 4 21 ovmpod ⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) )