fucass

Description: Associativity of natural transformation composition. Remark 6.14(b) in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucass.q	$⊢ Q = C FuncCat D$
	fucass.n	$⊢ N = C Nat D$
	fucass.x	$⊢ \underset{˙}{∙} = comp (Q)$
	fucass.r	$⊢ φ \to R \in (F N G)$
	fucass.s	$⊢ φ \to S \in (G N H)$
	fucass.t	$⊢ φ \to T \in (H N K)$
Assertion	fucass	$⊢ φ \to (T (⟨G, H⟩ \underset{˙}{∙} K) S) (⟨F, G⟩ \underset{˙}{∙} K) R = T (⟨F, H⟩ \underset{˙}{∙} K) (S (⟨F, G⟩ \underset{˙}{∙} H) R)$

Proof

Step	Hyp	Ref	Expression
1		fucass.q	$⊢ Q = C FuncCat D$
2		fucass.n	$⊢ N = C Nat D$
3		fucass.x	$⊢ \underset{˙}{∙} = comp (Q)$
4		fucass.r	$⊢ φ \to R \in (F N G)$
5		fucass.s	$⊢ φ \to S \in (G N H)$
6		fucass.t	$⊢ φ \to T \in (H N K)$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8		eqid	$⊢ Hom (D) = Hom (D)$
9		eqid	$⊢ comp (D) = comp (D)$
10	2	natrcl	$⊢ R \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$
11	4 10	syl	$⊢ φ \to (F \in (C Func D) \land G \in (C Func D))$
12	11	simpld	$⊢ φ \to F \in (C Func D)$
13		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
14	12 13	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
15	14	simprd	$⊢ φ \to D \in Cat$
16	15	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
17		eqid	$⊢ {Base}_{C} = {Base}_{C}$
18		relfunc	$⊢ Rel (C Func D)$
19		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
20	18 12 19	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
21	17 7 20	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
22	21	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
23	11	simprd	$⊢ φ \to G \in (C Func D)$
24		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
25	18 23 24	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
26	17 7 25	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
27	26	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{D}$
28	2	natrcl	$⊢ T \in (H N K) \to (H \in (C Func D) \land K \in (C Func D))$
29	6 28	syl	$⊢ φ \to (H \in (C Func D) \land K \in (C Func D))$
30	29	simpld	$⊢ φ \to H \in (C Func D)$
31		1st2ndbr	$⊢ (Rel (C Func D) \land H \in (C Func D)) \to 1^{st} (H) (C Func D) 2^{nd} (H)$
32	18 30 31	sylancr	$⊢ φ \to 1^{st} (H) (C Func D) 2^{nd} (H)$
33	17 7 32	funcf1	$⊢ φ \to 1^{st} (H) : {Base}_{C} ⟶ {Base}_{D}$
34	33	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (H) (x) \in {Base}_{D}$
35	2 4	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
36	35	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
37		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
38	2 36 17 8 37	natcl	$⊢ (φ \land x \in {Base}_{C}) \to R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (G) (x))$
39	2 5	nat1st2nd	$⊢ φ \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (H), 2^{nd} (H)⟩)$
40	39	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (H), 2^{nd} (H)⟩)$
41	2 40 17 8 37	natcl	$⊢ (φ \land x \in {Base}_{C}) \to S (x) \in (1^{st} (G) (x) Hom (D) 1^{st} (H) (x))$
42	29	simprd	$⊢ φ \to K \in (C Func D)$
43		1st2ndbr	$⊢ (Rel (C Func D) \land K \in (C Func D)) \to 1^{st} (K) (C Func D) 2^{nd} (K)$
44	18 42 43	sylancr	$⊢ φ \to 1^{st} (K) (C Func D) 2^{nd} (K)$
45	17 7 44	funcf1	$⊢ φ \to 1^{st} (K) : {Base}_{C} ⟶ {Base}_{D}$
46	45	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (K) (x) \in {Base}_{D}$
47	2 6	nat1st2nd	$⊢ φ \to T \in (⟨1^{st} (H), 2^{nd} (H)⟩ N ⟨1^{st} (K), 2^{nd} (K)⟩)$
48	47	adantr	$⊢ (φ \land x \in {Base}_{C}) \to T \in (⟨1^{st} (H), 2^{nd} (H)⟩ N ⟨1^{st} (K), 2^{nd} (K)⟩)$
49	2 48 17 8 37	natcl	$⊢ (φ \land x \in {Base}_{C}) \to T (x) \in (1^{st} (H) (x) Hom (D) 1^{st} (K) (x))$
50	7 8 9 16 22 27 34 38 41 46 49	catass	$⊢ (φ \land x \in {Base}_{C}) \to (T (x) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) S (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (K) (x)) R (x) = T (x) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) (S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x))$
51	5	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (G N H)$
52	6	adantr	$⊢ (φ \land x \in {Base}_{C}) \to T \in (H N K)$
53	1 2 17 9 3 51 52 37	fuccoval	$⊢ (φ \land x \in {Base}_{C}) \to (T (⟨G, H⟩ \underset{˙}{∙} K) S) (x) = T (x) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) S (x)$
54	53	oveq1d	$⊢ (φ \land x \in {Base}_{C}) \to (T (⟨G, H⟩ \underset{˙}{∙} K) S) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (K) (x)) R (x) = (T (x) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) S (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (K) (x)) R (x)$
55	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (F N G)$
56	1 2 17 9 3 55 51 37	fuccoval	$⊢ (φ \land x \in {Base}_{C}) \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x) = S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x)$
57	56	oveq2d	$⊢ (φ \land x \in {Base}_{C}) \to T (x) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x) = T (x) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) (S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x))$
58	50 54 57	3eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to (T (⟨G, H⟩ \underset{˙}{∙} K) S) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (K) (x)) R (x) = T (x) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x)$
59	58	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (T (⟨G, H⟩ \underset{˙}{∙} K) S) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (K) (x)) R (x)) = (x \in {Base}_{C} ⟼ T (x) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x))$
60	1 2 3 5 6	fuccocl	$⊢ φ \to T (⟨G, H⟩ \underset{˙}{∙} K) S \in (G N K)$
61	1 2 17 9 3 4 60	fucco	$⊢ φ \to (T (⟨G, H⟩ \underset{˙}{∙} K) S) (⟨F, G⟩ \underset{˙}{∙} K) R = (x \in {Base}_{C} ⟼ (T (⟨G, H⟩ \underset{˙}{∙} K) S) (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (K) (x)) R (x))$
62	1 2 3 4 5	fuccocl	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R \in (F N H)$
63	1 2 17 9 3 62 6	fucco	$⊢ φ \to T (⟨F, H⟩ \underset{˙}{∙} K) (S (⟨F, G⟩ \underset{˙}{∙} H) R) = (x \in {Base}_{C} ⟼ T (x) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (K) (x)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x))$
64	59 61 63	3eqtr4d	$⊢ φ \to (T (⟨G, H⟩ \underset{˙}{∙} K) S) (⟨F, G⟩ \underset{˙}{∙} K) R = T (⟨F, H⟩ \underset{˙}{∙} K) (S (⟨F, G⟩ \underset{˙}{∙} H) R)$

Metamath Proof Explorer

Theorem fucass

Proof