Metamath Proof Explorer

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	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
		fuco23a.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
		fuco23a.x	$⊢ φ \to X \in {Base}_{C}$
		fuco23a.p	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
		fuco23a.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
		fuco23a.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
		fuco23a.o	$⊢ φ \to \underset{˙}{*} = ⟨K (F (X)), R (F (X))⟩ comp (E) R (M (X))$
	Assertion	fuco23a	$⊢ φ \to (B (U P V) A) (X) = (F (X) S M (X)) (A (X)) \underset{˙}{*} B (F (X))$

Proof

Step	Hyp	Ref	Expression
1		fuco23a.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
2		fuco23a.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
3		fuco23a.x	$⊢ φ \to X \in {Base}_{C}$
4		fuco23a.p	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
5		fuco23a.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
6		fuco23a.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
7		fuco23a.o	$⊢ φ \to \underset{˙}{*} = ⟨K (F (X)), R (F (X))⟩ comp (E) R (M (X))$
8		eqid	$⊢ comp (E) = comp (E)$
9	1 2 3 8	fuco23alem	$⊢ φ \to B (M (X)) (⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))) (F (X) L M (X)) (A (X)) = (F (X) S M (X)) (A (X)) (⟨K (F (X)), R (F (X))⟩ comp (E) R (M (X))) B (F (X))$
10		eqidd	$⊢ φ \to ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X)) = ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))$
11	4 5 6 1 2 3 10	fuco23	$⊢ φ \to (B (U P V) A) (X) = B (M (X)) (⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))) (F (X) L M (X)) (A (X))$
12	7	oveqd	$⊢ φ \to (F (X) S M (X)) (A (X)) \underset{˙}{*} B (F (X)) = (F (X) S M (X)) (A (X)) (⟨K (F (X)), R (F (X))⟩ comp (E) R (M (X))) B (F (X))$
13	9 11 12	3eqtr4d	$⊢ φ \to (B (U P V) A) (X) = (F (X) S M (X)) (A (X)) \underset{˙}{*} B (F (X))$