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	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucass.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucass.x	⊢ ∙ = ( comp ‘ 𝑄 )
	fucass.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
	fucass.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
	fucass.t	⊢ ( 𝜑 → 𝑇 ∈ ( 𝐻 𝑁 𝐾 ) )
Assertion	fucass	⊢ ( 𝜑 → ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐾 ) 𝑅 ) = ( 𝑇 ( ⟨ 𝐹 , 𝐻 ⟩ ∙ 𝐾 ) ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucass.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucass.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		fucass.x	⊢ ∙ = ( comp ‘ 𝑄 )
4		fucass.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
5		fucass.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
6		fucass.t	⊢ ( 𝜑 → 𝑇 ∈ ( 𝐻 𝑁 𝐾 ) )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
10	2	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
11	4 10	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
12	11	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
13		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
15	14	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
17		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
18		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
19		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
20	18 12 19	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
21	17 7 20	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
22	21	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
23	11	simprd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
24		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
25	18 23 24	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
26	17 7 25	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
27	26	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
28	2	natrcl	⊢ ( 𝑇 ∈ ( 𝐻 𝑁 𝐾 ) → ( 𝐻 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐾 ∈ ( 𝐶 Func 𝐷 ) ) )
29	6 28	syl	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐾 ∈ ( 𝐶 Func 𝐷 ) ) )
30	29	simpld	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐶 Func 𝐷 ) )
31		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐻 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
32	18 30 31	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐻 ) )
33	17 7 32	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐻 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
34	33	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
35	2 4	nat1st2nd	⊢ ( 𝜑 → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
38	2 36 17 8 37	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
39	2 5	nat1st2nd	⊢ ( 𝜑 → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ ) )
41	2 40 17 8 37	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) )
42	29	simprd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐶 Func 𝐷 ) )
43		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐾 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐾 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐾 ) )
44	18 42 43	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐾 ) )
45	17 7 44	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
46	45	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
47	2 6	nat1st2nd	⊢ ( 𝜑 → 𝑇 ∈ ( ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑇 ∈ ( ⟨ ( 1^st ‘ 𝐻 ) , ( 2^nd ‘ 𝐻 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ) )
49	2 48 17 8 37	natcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑇 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) )
50	7 8 9 16 22 27 34 38 41 46 49	catass	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
51	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
52	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑇 ∈ ( 𝐻 𝑁 𝐾 ) )
53	1 2 17 9 3 51 52 37	fuccoval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) )
54	53	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑆 ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) )
55	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
56	1 2 17 9 3 55 51 37	fuccoval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) )
57	56	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
58	50 54 57	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) )
59	58	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) ) )
60	1 2 3 5 6	fuccocl	⊢ ( 𝜑 → ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ∈ ( 𝐺 𝑁 𝐾 ) )
61	1 2 17 9 3 4 60	fucco	⊢ ( 𝜑 → ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐾 ) 𝑅 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
62	1 2 3 4 5	fuccocl	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ∈ ( 𝐹 𝑁 𝐻 ) )
63	1 2 17 9 3 62 6	fucco	⊢ ( 𝜑 → ( 𝑇 ( ⟨ 𝐹 , 𝐻 ⟩ ∙ 𝐾 ) ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑇 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐾 ) ‘ 𝑥 ) ) ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑥 ) ) ) )
64	59 61 63	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑇 ( ⟨ 𝐺 , 𝐻 ⟩ ∙ 𝐾 ) 𝑆 ) ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐾 ) 𝑅 ) = ( 𝑇 ( ⟨ 𝐹 , 𝐻 ⟩ ∙ 𝐾 ) ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ) )

Metamath Proof Explorer

Theorem fucass

Proof