catass

Description: Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	catcocl.b	$⊢ B = {Base}_{C}$
	catcocl.h	$⊢ H = Hom (C)$
	catcocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	catcocl.c	$⊢ φ \to C \in Cat$
	catcocl.x	$⊢ φ \to X \in B$
	catcocl.y	$⊢ φ \to Y \in B$
	catcocl.z	$⊢ φ \to Z \in B$
	catcocl.f	$⊢ φ \to F \in (X H Y)$
	catcocl.g	$⊢ φ \to G \in (Y H Z)$
	catass.w	$⊢ φ \to W \in B$
	catass.g	$⊢ φ \to K \in (Z H W)$
Assertion	catass	$⊢ φ \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F)$

Proof

Step	Hyp	Ref	Expression
1		catcocl.b	$⊢ B = {Base}_{C}$
2		catcocl.h	$⊢ H = Hom (C)$
3		catcocl.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		catcocl.c	$⊢ φ \to C \in Cat$
5		catcocl.x	$⊢ φ \to X \in B$
6		catcocl.y	$⊢ φ \to Y \in B$
7		catcocl.z	$⊢ φ \to Z \in B$
8		catcocl.f	$⊢ φ \to F \in (X H Y)$
9		catcocl.g	$⊢ φ \to G \in (Y H Z)$
10		catass.w	$⊢ φ \to W \in B$
11		catass.g	$⊢ φ \to K \in (Z H W)$
12	1 2 3	iscat	$⊢ C \in Cat \to (C \in Cat \leftrightarrow \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))))$
13	12	ibi	$⊢ C \in Cat \to \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
14	4 13	syl	$⊢ φ \to \forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)))$
15	6	adantr	$⊢ (φ \land x = X) \to Y \in B$
16	7	ad2antrr	$⊢ ((φ \land x = X) \land y = Y) \to Z \in B$
17	8	ad3antrrr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to F \in (X H Y)$
18		simpllr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x = X$
19		simplr	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to y = Y$
20	18 19	oveq12d	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to x H y = X H Y$
21	17 20	eleqtrrd	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to F \in (x H y)$
22	9	ad4antr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to G \in (Y H Z)$
23		simpllr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to y = Y$
24		simplr	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to z = Z$
25	23 24	oveq12d	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to y H z = Y H Z$
26	22 25	eleqtrrd	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to G \in (y H z)$
27	10	ad5antr	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to W \in B$
28	11	ad6antr	$⊢ ((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \to K \in (Z H W)$
29		simp-4r	$⊢ ((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \to z = Z$
30		simpr	$⊢ ((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \to w = W$
31	29 30	oveq12d	$⊢ ((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \to z H w = Z H W$
32	28 31	eleqtrrd	$⊢ ((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \to K \in (z H w)$
33		simp-7r	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to x = X$
34		simp-6r	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to y = Y$
35	33 34	opeq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨x, y⟩ = ⟨X, Y⟩$
36		simplr	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to w = W$
37	35 36	oveq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨x, y⟩ \underset{˙}{\cdot} w = ⟨X, Y⟩ \underset{˙}{\cdot} W$
38		simp-5r	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to z = Z$
39	34 38	opeq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨y, z⟩ = ⟨Y, Z⟩$
40	39 36	oveq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨y, z⟩ \underset{˙}{\cdot} w = ⟨Y, Z⟩ \underset{˙}{\cdot} W$
41		simpr	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to k = K$
42		simpllr	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to g = G$
43	40 41 42	oveq123d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to k (⟨y, z⟩ \underset{˙}{\cdot} w) g = K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G$
44		simp-4r	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to f = F$
45	37 43 44	oveq123d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F$
46	33 38	opeq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨x, z⟩ = ⟨X, Z⟩$
47	46 36	oveq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨x, z⟩ \underset{˙}{\cdot} w = ⟨X, Z⟩ \underset{˙}{\cdot} W$
48	35 38	oveq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ⟨x, y⟩ \underset{˙}{\cdot} z = ⟨X, Y⟩ \underset{˙}{\cdot} Z$
49	48 42 44	oveq123d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F$
50	47 41 49	oveq123d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F)$
51	45 50	eqeq12d	$⊢ (((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \land k = K) \to ((k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \leftrightarrow (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
52	32 51	rspcdv	$⊢ ((((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \land w = W) \to (\forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
53	27 52	rspcimdv	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to (\forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
54	53	adantld	$⊢ (((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \land g = G) \to ((g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
55	26 54	rspcimdv	$⊢ ((((φ \land x = X) \land y = Y) \land z = Z) \land f = F) \to (\forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
56	21 55	rspcimdv	$⊢ (((φ \land x = X) \land y = Y) \land z = Z) \to (\forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
57	16 56	rspcimdv	$⊢ ((φ \land x = X) \land y = Y) \to (\forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
58	15 57	rspcimdv	$⊢ (φ \land x = X) \to (\forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
59	58	adantld	$⊢ (φ \land x = X) \to ((\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
60	5 59	rspcimdv	$⊢ φ \to (\forall x \in B (\exists g \in (x H x) \forall y \in B (\forall f \in (y H x) g (⟨y, x⟩ \underset{˙}{\cdot} x) f = f \land \forall f \in (x H y) f (⟨x, x⟩ \underset{˙}{\cdot} y) g = f) \land \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z) \land \forall w \in B \forall k \in (z H w) (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f))) \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F))$
61	14 60	mpd	$⊢ φ \to (K (⟨Y, Z⟩ \underset{˙}{\cdot} W) G) (⟨X, Y⟩ \underset{˙}{\cdot} W) F = K (⟨X, Z⟩ \underset{˙}{\cdot} W) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F)$

Metamath Proof Explorer

Theorem catass

Proof