Theorem fuco23a

Description: The morphism part of the functor composition bifunctor. An alternate definition of o.F . See also fuco23 . (Contributed by Zhi Wang, 3-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fuco23a.a	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
2		fuco23a.b	⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
3		fuco23a.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
4		fuco23a.p	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
5		fuco23a.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
6		fuco23a.v	⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
7		fuco23a.o	⊢ ( 𝜑 → ∗ = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
8		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
9	1 2 3 8	fuco23alem	⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( 𝐵 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
10		eqidd	⊢ ( 𝜑 → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
11	4 5 6 1 2 3 10	fuco23	⊢ ( 𝜑 → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
12	7	oveqd	⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∗ ( 𝐵 ‘ ( 𝐹 ‘ 𝑋 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝐹 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( 𝐵 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
13	9 11 12	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑋 ) = ( ( ( ( 𝐹 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∗ ( 𝐵 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )