arwass

Description: Associativity of composition in a category using arrow notation. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwlid.h	$⊢ H = {Hom}_{a} (C)$
	arwlid.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
	arwlid.a	$⊢ \underset{˙}{1} = {Id}_{a} (C)$
	arwlid.f	$⊢ φ \to F \in (X H Y)$
	arwass.g	$⊢ φ \to G \in (Y H Z)$
	arwass.k	$⊢ φ \to K \in (Z H W)$
Assertion	arwass	$⊢ φ \to (K \underset{˙}{\cdot} G) \underset{˙}{\cdot} F = K \underset{˙}{\cdot} (G \underset{˙}{\cdot} F)$

Proof

Step	Hyp	Ref	Expression
1		arwlid.h	$⊢ H = {Hom}_{a} (C)$
2		arwlid.o	$⊢ \underset{˙}{\cdot} = {comp}_{a} (C)$
3		arwlid.a	$⊢ \underset{˙}{1} = {Id}_{a} (C)$
4		arwlid.f	$⊢ φ \to F \in (X H Y)$
5		arwass.g	$⊢ φ \to G \in (Y H Z)$
6		arwass.k	$⊢ φ \to K \in (Z H W)$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10	1	homarcl	$⊢ F \in (X H Y) \to C \in Cat$
11	4 10	syl	$⊢ φ \to C \in Cat$
12	1 7	homarcl2	$⊢ F \in (X H Y) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
13	4 12	syl	$⊢ φ \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
14	13	simpld	$⊢ φ \to X \in {Base}_{C}$
15	13	simprd	$⊢ φ \to Y \in {Base}_{C}$
16	1 7	homarcl2	$⊢ K \in (Z H W) \to (Z \in {Base}_{C} \land W \in {Base}_{C})$
17	6 16	syl	$⊢ φ \to (Z \in {Base}_{C} \land W \in {Base}_{C})$
18	17	simpld	$⊢ φ \to Z \in {Base}_{C}$
19	1 8	homahom	$⊢ F \in (X H Y) \to 2^{nd} (F) \in (X Hom (C) Y)$
20	4 19	syl	$⊢ φ \to 2^{nd} (F) \in (X Hom (C) Y)$
21	1 8	homahom	$⊢ G \in (Y H Z) \to 2^{nd} (G) \in (Y Hom (C) Z)$
22	5 21	syl	$⊢ φ \to 2^{nd} (G) \in (Y Hom (C) Z)$
23	17	simprd	$⊢ φ \to W \in {Base}_{C}$
24	1 8	homahom	$⊢ K \in (Z H W) \to 2^{nd} (K) \in (Z Hom (C) W)$
25	6 24	syl	$⊢ φ \to 2^{nd} (K) \in (Z Hom (C) W)$
26	7 8 9 11 14 15 18 20 22 23 25	catass	$⊢ φ \to (2^{nd} (K) (⟨Y, Z⟩ comp (C) W) 2^{nd} (G)) (⟨X, Y⟩ comp (C) W) 2^{nd} (F) = 2^{nd} (K) (⟨X, Z⟩ comp (C) W) (2^{nd} (G) (⟨X, Y⟩ comp (C) Z) 2^{nd} (F))$
27	2 1 5 6 9	coa2	$⊢ φ \to 2^{nd} (K \underset{˙}{\cdot} G) = 2^{nd} (K) (⟨Y, Z⟩ comp (C) W) 2^{nd} (G)$
28	27	oveq1d	$⊢ φ \to 2^{nd} (K \underset{˙}{\cdot} G) (⟨X, Y⟩ comp (C) W) 2^{nd} (F) = (2^{nd} (K) (⟨Y, Z⟩ comp (C) W) 2^{nd} (G)) (⟨X, Y⟩ comp (C) W) 2^{nd} (F)$
29	2 1 4 5 9	coa2	$⊢ φ \to 2^{nd} (G \underset{˙}{\cdot} F) = 2^{nd} (G) (⟨X, Y⟩ comp (C) Z) 2^{nd} (F)$
30	29	oveq2d	$⊢ φ \to 2^{nd} (K) (⟨X, Z⟩ comp (C) W) 2^{nd} (G \underset{˙}{\cdot} F) = 2^{nd} (K) (⟨X, Z⟩ comp (C) W) (2^{nd} (G) (⟨X, Y⟩ comp (C) Z) 2^{nd} (F))$
31	26 28 30	3eqtr4d	$⊢ φ \to 2^{nd} (K \underset{˙}{\cdot} G) (⟨X, Y⟩ comp (C) W) 2^{nd} (F) = 2^{nd} (K) (⟨X, Z⟩ comp (C) W) 2^{nd} (G \underset{˙}{\cdot} F)$
32	31	oteq3d	$⊢ φ \to ⟨X, W, 2^{nd} (K \underset{˙}{\cdot} G) (⟨X, Y⟩ comp (C) W) 2^{nd} (F)⟩ = ⟨X, W, 2^{nd} (K) (⟨X, Z⟩ comp (C) W) 2^{nd} (G \underset{˙}{\cdot} F)⟩$
33	2 1 5 6	coahom	$⊢ φ \to K \underset{˙}{\cdot} G \in (Y H W)$
34	2 1 4 33 9	coaval	$⊢ φ \to (K \underset{˙}{\cdot} G) \underset{˙}{\cdot} F = ⟨X, W, 2^{nd} (K \underset{˙}{\cdot} G) (⟨X, Y⟩ comp (C) W) 2^{nd} (F)⟩$
35	2 1 4 5	coahom	$⊢ φ \to G \underset{˙}{\cdot} F \in (X H Z)$
36	2 1 35 6 9	coaval	$⊢ φ \to K \underset{˙}{\cdot} (G \underset{˙}{\cdot} F) = ⟨X, W, 2^{nd} (K) (⟨X, Z⟩ comp (C) W) 2^{nd} (G \underset{˙}{\cdot} F)⟩$
37	32 34 36	3eqtr4d	$⊢ φ \to (K \underset{˙}{\cdot} G) \underset{˙}{\cdot} F = K \underset{˙}{\cdot} (G \underset{˙}{\cdot} F)$

Metamath Proof Explorer

Theorem arwass

Proof