cofuass

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

	Ref	Expression
Hypotheses	cofuass.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	cofuass.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐷 Func 𝐸 ) )
	cofuass.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐸 Func 𝐹 ) )
Assertion	cofuass	⊢ ( 𝜑 → ( ( 𝐾 ∘_func 𝐻 ) ∘_func 𝐺 ) = ( 𝐾 ∘_func ( 𝐻 ∘_func 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofuass.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
2		cofuass.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐷 Func 𝐸 ) )
3		cofuass.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐸 Func 𝐹 ) )
4		coass	⊢ ( ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐻 ) ) ∘ ( 1^st ‘ 𝐺 ) ) = ( ( 1^st ‘ 𝐾 ) ∘ ( ( 1^st ‘ 𝐻 ) ∘ ( 1^st ‘ 𝐺 ) ) )
5		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6	5 2 3	cofu1st	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐾 ∘_func 𝐻 ) ) = ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐻 ) ) )
7	6	coeq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐾 ∘_func 𝐻 ) ) ∘ ( 1^st ‘ 𝐺 ) ) = ( ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐻 ) ) ∘ ( 1^st ‘ 𝐺 ) ) )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9	8 1 2	cofu1st	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) = ( ( 1^st ‘ 𝐻 ) ∘ ( 1^st ‘ 𝐺 ) ) )
10	9	coeq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ) = ( ( 1^st ‘ 𝐾 ) ∘ ( ( 1^st ‘ 𝐻 ) ∘ ( 1^st ‘ 𝐺 ) ) ) )
11	4 7 10	3eqtr4a	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐾 ∘_func 𝐻 ) ) ∘ ( 1^st ‘ 𝐺 ) ) = ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ) )
12		coass	⊢ ( ( ( ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) )
13	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝐻 ∈ ( 𝐷 Func 𝐸 ) )
14	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝐾 ∈ ( 𝐸 Func 𝐹 ) )
15		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
16		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
17	15 1 16	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
18	17	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
19	8 5 18	funcf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
20		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
21	19 20	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
22		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
23	19 22	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
24	5 13 14 21 23	cofu2nd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐻 ) ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
25	24	coeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐻 ) ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) = ( ( ( ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) )
26	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
27	8 26 13 20	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) )
28	8 26 13 22	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
29	27 28	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
30	8 26 13 20 22	cofu2nd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2^nd ‘ ( 𝐻 ∘_func 𝐺 ) ) 𝑦 ) = ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) )
31	29 30	coeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ ( 𝐻 ∘_func 𝐺 ) ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝐻 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∘ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐻 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) ) )
32	12 25 31	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐻 ) ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ ( 𝐻 ∘_func 𝐺 ) ) 𝑦 ) ) )
33	32	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐻 ) ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ ( 𝐻 ∘_func 𝐺 ) ) 𝑦 ) ) ) )
34	11 33	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( 𝐾 ∘_func 𝐻 ) ) ∘ ( 1^st ‘ 𝐺 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐻 ) ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ ( 𝐻 ∘_func 𝐺 ) ) 𝑦 ) ) ) ⟩ )
35	2 3	cofucl	⊢ ( 𝜑 → ( 𝐾 ∘_func 𝐻 ) ∈ ( 𝐷 Func 𝐹 ) )
36	8 1 35	cofuval	⊢ ( 𝜑 → ( ( 𝐾 ∘_func 𝐻 ) ∘_func 𝐺 ) = ⟨ ( ( 1^st ‘ ( 𝐾 ∘_func 𝐻 ) ) ∘ ( 1^st ‘ 𝐺 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐻 ) ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ) ) ⟩ )
37	1 2	cofucl	⊢ ( 𝜑 → ( 𝐻 ∘_func 𝐺 ) ∈ ( 𝐶 Func 𝐸 ) )
38	8 37 3	cofuval	⊢ ( 𝜑 → ( 𝐾 ∘_func ( 𝐻 ∘_func 𝐺 ) ) = ⟨ ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ ( 𝐻 ∘_func 𝐺 ) ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ ( 𝐻 ∘_func 𝐺 ) ) 𝑦 ) ) ) ⟩ )
39	34 36 38	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐾 ∘_func 𝐻 ) ∘_func 𝐺 ) = ( 𝐾 ∘_func ( 𝐻 ∘_func 𝐺 ) ) )

Metamath Proof Explorer

Theorem cofuass

Proof