cofu2

Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	cofuval.b	$⊢ B = {Base}_{C}$
	cofuval.f	$⊢ φ \to F \in (C Func D)$
	cofuval.g	$⊢ φ \to G \in (D Func E)$
	cofu2nd.x	$⊢ φ \to X \in B$
	cofu2nd.y	$⊢ φ \to Y \in B$
	cofu2.h	$⊢ H = Hom (C)$
	cofu2.y	$⊢ φ \to R \in (X H Y)$
Assertion	cofu2	$⊢ φ \to (X 2^{nd} (G \circ_{func} F) Y) (R) = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) ((X 2^{nd} (F) Y) (R))$

Step	Hyp	Ref	Expression
1		cofuval.b	$⊢ B = {Base}_{C}$
2		cofuval.f	$⊢ φ \to F \in (C Func D)$
3		cofuval.g	$⊢ φ \to G \in (D Func E)$
4		cofu2nd.x	$⊢ φ \to X \in B$
5		cofu2nd.y	$⊢ φ \to Y \in B$
6		cofu2.h	$⊢ H = Hom (C)$
7		cofu2.y	$⊢ φ \to R \in (X H Y)$
8	1 2 3 4 5	cofu2nd	$⊢ φ \to X 2^{nd} (G \circ_{func} F) Y = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)$
9	8	fveq1d	$⊢ φ \to (X 2^{nd} (G \circ_{func} F) Y) (R) = ((1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)) (R)$
10		eqid	$⊢ Hom (D) = Hom (D)$
11		relfunc	$⊢ Rel (C Func D)$
12		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
13	11 2 12	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
14	1 6 10 13 4 5	funcf2	$⊢ φ \to (X 2^{nd} (F) Y) : X H Y ⟶ 1^{st} (F) (X) Hom (D) 1^{st} (F) (Y)$
15		fvco3	$⊢ ((X 2^{nd} (F) Y) : X H Y ⟶ 1^{st} (F) (X) Hom (D) 1^{st} (F) (Y) \land R \in (X H Y)) \to ((1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)) (R) = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) ((X 2^{nd} (F) Y) (R))$
16	14 7 15	syl2anc	$⊢ φ \to ((1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)) (R) = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) ((X 2^{nd} (F) Y) (R))$
17	9 16	eqtrd	$⊢ φ \to (X 2^{nd} (G \circ_{func} F) Y) (R) = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) ((X 2^{nd} (F) Y) (R))$

Metamath Proof Explorer