cofuass

Description: Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuass.g	$⊢ φ \to G \in (C Func D)$
	cofuass.h	$⊢ φ \to H \in (D Func E)$
	cofuass.k	$⊢ φ \to K \in (E Func F)$
Assertion	cofuass	$⊢ φ \to (K \circ_{func} H) \circ_{func} G = K \circ_{func} (H \circ_{func} G)$

Proof

Step	Hyp	Ref	Expression
1		cofuass.g	$⊢ φ \to G \in (C Func D)$
2		cofuass.h	$⊢ φ \to H \in (D Func E)$
3		cofuass.k	$⊢ φ \to K \in (E Func F)$
4		coass	$⊢ (1^{st} (K) \circ 1^{st} (H)) \circ 1^{st} (G) = 1^{st} (K) \circ (1^{st} (H) \circ 1^{st} (G))$
5		eqid	$⊢ {Base}_{D} = {Base}_{D}$
6	5 2 3	cofu1st	$⊢ φ \to 1^{st} (K \circ_{func} H) = 1^{st} (K) \circ 1^{st} (H)$
7	6	coeq1d	$⊢ φ \to 1^{st} (K \circ_{func} H) \circ 1^{st} (G) = (1^{st} (K) \circ 1^{st} (H)) \circ 1^{st} (G)$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9	8 1 2	cofu1st	$⊢ φ \to 1^{st} (H \circ_{func} G) = 1^{st} (H) \circ 1^{st} (G)$
10	9	coeq2d	$⊢ φ \to 1^{st} (K) \circ 1^{st} (H \circ_{func} G) = 1^{st} (K) \circ (1^{st} (H) \circ 1^{st} (G))$
11	4 7 10	3eqtr4a	$⊢ φ \to 1^{st} (K \circ_{func} H) \circ 1^{st} (G) = 1^{st} (K) \circ 1^{st} (H \circ_{func} G)$
12		coass	$⊢ ((1^{st} (H) (1^{st} (G) (x)) 2^{nd} (K) 1^{st} (H) (1^{st} (G) (y))) \circ (1^{st} (G) (x) 2^{nd} (H) 1^{st} (G) (y))) \circ (x 2^{nd} (G) y) = (1^{st} (H) (1^{st} (G) (x)) 2^{nd} (K) 1^{st} (H) (1^{st} (G) (y))) \circ ((1^{st} (G) (x) 2^{nd} (H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y))$
13	2	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to H \in (D Func E)$
14	3	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to K \in (E Func F)$
15		relfunc	$⊢ Rel (C Func D)$
16		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
17	15 1 16	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
18	17	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
19	8 5 18	funcf1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
20		simp2	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x \in {Base}_{C}$
21	19 20	ffvelrnd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{D}$
22		simp3	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to y \in {Base}_{C}$
23	19 22	ffvelrnd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (G) (y) \in {Base}_{D}$
24	5 13 14 21 23	cofu2nd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (G) (x) 2^{nd} (K \circ_{func} H) 1^{st} (G) (y) = (1^{st} (H) (1^{st} (G) (x)) 2^{nd} (K) 1^{st} (H) (1^{st} (G) (y))) \circ (1^{st} (G) (x) 2^{nd} (H) 1^{st} (G) (y))$
25	24	coeq1d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (1^{st} (G) (x) 2^{nd} (K \circ_{func} H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y) = ((1^{st} (H) (1^{st} (G) (x)) 2^{nd} (K) 1^{st} (H) (1^{st} (G) (y))) \circ (1^{st} (G) (x) 2^{nd} (H) 1^{st} (G) (y))) \circ (x 2^{nd} (G) y)$
26	1	3ad2ant1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to G \in (C Func D)$
27	8 26 13 20	cofu1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (H \circ_{func} G) (x) = 1^{st} (H) (1^{st} (G) (x))$
28	8 26 13 22	cofu1	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (H \circ_{func} G) (y) = 1^{st} (H) (1^{st} (G) (y))$
29	27 28	oveq12d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to 1^{st} (H \circ_{func} G) (x) 2^{nd} (K) 1^{st} (H \circ_{func} G) (y) = 1^{st} (H) (1^{st} (G) (x)) 2^{nd} (K) 1^{st} (H) (1^{st} (G) (y))$
30	8 26 13 20 22	cofu2nd	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x 2^{nd} (H \circ_{func} G) y = (1^{st} (G) (x) 2^{nd} (H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y)$
31	29 30	coeq12d	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (1^{st} (H \circ_{func} G) (x) 2^{nd} (K) 1^{st} (H \circ_{func} G) (y)) \circ (x 2^{nd} (H \circ_{func} G) y) = (1^{st} (H) (1^{st} (G) (x)) 2^{nd} (K) 1^{st} (H) (1^{st} (G) (y))) \circ ((1^{st} (G) (x) 2^{nd} (H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y))$
32	12 25 31	3eqtr4a	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (1^{st} (G) (x) 2^{nd} (K \circ_{func} H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y) = (1^{st} (H \circ_{func} G) (x) 2^{nd} (K) 1^{st} (H \circ_{func} G) (y)) \circ (x 2^{nd} (H \circ_{func} G) y)$
33	32	mpoeq3dva	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (G) (x) 2^{nd} (K \circ_{func} H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (H \circ_{func} G) (x) 2^{nd} (K) 1^{st} (H \circ_{func} G) (y)) \circ (x 2^{nd} (H \circ_{func} G) y))$
34	11 33	opeq12d	$⊢ φ \to ⟨1^{st} (K \circ_{func} H) \circ 1^{st} (G), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (G) (x) 2^{nd} (K \circ_{func} H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y))⟩ = ⟨1^{st} (K) \circ 1^{st} (H \circ_{func} G), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (H \circ_{func} G) (x) 2^{nd} (K) 1^{st} (H \circ_{func} G) (y)) \circ (x 2^{nd} (H \circ_{func} G) y))⟩$
35	2 3	cofucl	$⊢ φ \to K \circ_{func} H \in (D Func F)$
36	8 1 35	cofuval	$⊢ φ \to (K \circ_{func} H) \circ_{func} G = ⟨1^{st} (K \circ_{func} H) \circ 1^{st} (G), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (G) (x) 2^{nd} (K \circ_{func} H) 1^{st} (G) (y)) \circ (x 2^{nd} (G) y))⟩$
37	1 2	cofucl	$⊢ φ \to H \circ_{func} G \in (C Func E)$
38	8 37 3	cofuval	$⊢ φ \to K \circ_{func} (H \circ_{func} G) = ⟨1^{st} (K) \circ 1^{st} (H \circ_{func} G), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (H \circ_{func} G) (x) 2^{nd} (K) 1^{st} (H \circ_{func} G) (y)) \circ (x 2^{nd} (H \circ_{func} G) y))⟩$
39	34 36 38	3eqtr4d	$⊢ φ \to (K \circ_{func} H) \circ_{func} G = K \circ_{func} (H \circ_{func} G)$

Metamath Proof Explorer

Theorem cofuass

Proof