fuco112xa

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. A morphism is mapped by two functors in succession. (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco11.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco11.f	$⊢ φ \to F (C Func D) G$
	fuco11.k	$⊢ φ \to K (D Func E) L$
	fuco11.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
	fuco111x.x	$⊢ φ \to X \in {Base}_{C}$
	fuco112x.y	$⊢ φ \to Y \in {Base}_{C}$
	fuco112xa.a	$⊢ φ \to A \in (X Hom (C) Y)$
Assertion	fuco112xa	$⊢ φ \to (X 2^{nd} (O (U)) Y) (A) = (F (X) L F (Y)) ((X G Y) (A))$

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	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 \|-
2		fuco11.f	$⊢ φ \to F (C Func D) G$
3		fuco11.k	$⊢ φ \to K (D Func E) L$
4		fuco11.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
5		fuco111x.x	$⊢ φ \to X \in {Base}_{C}$
6		fuco112x.y	$⊢ φ \to Y \in {Base}_{C}$
7		fuco112xa.a	$⊢ φ \to A \in (X Hom (C) Y)$
8	1 2 3 4 5 6	fuco112x	$⊢ φ \to X 2^{nd} (O (U)) Y = (F (X) L F (Y)) \circ (X G Y)$
9	8	fveq1d	$⊢ φ \to (X 2^{nd} (O (U)) Y) (A) = ((F (X) L F (Y)) \circ (X G Y)) (A)$
10		eqid	$⊢ {Base}_{C} = {Base}_{C}$
11		eqid	$⊢ Hom (C) = Hom (C)$
12		eqid	$⊢ Hom (D) = Hom (D)$
13	10 11 12 2 5 6	funcf2	$⊢ φ \to (X G Y) : X Hom (C) Y ⟶ F (X) Hom (D) F (Y)$
14	13 7	fvco3d	$⊢ φ \to ((F (X) L F (Y)) \circ (X G Y)) (A) = (F (X) L F (Y)) ((X G Y) (A))$
15	9 14	eqtrd	$⊢ φ \to (X 2^{nd} (O (U)) Y) (A) = (F (X) L F (Y)) ((X G Y) (A))$

Metamath Proof Explorer

Theorem fuco112xa

Proof