Metamath Proof Explorer


Theorem cofuass

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

Ref Expression
Hypotheses cofuass.g φGCFuncD
cofuass.h φHDFuncE
cofuass.k φKEFuncF
Assertion cofuass φKfuncHfuncG=KfuncHfuncG

Proof

Step Hyp Ref Expression
1 cofuass.g φGCFuncD
2 cofuass.h φHDFuncE
3 cofuass.k φKEFuncF
4 coass 1stK1stH1stG=1stK1stH1stG
5 eqid BaseD=BaseD
6 5 2 3 cofu1st φ1stKfuncH=1stK1stH
7 6 coeq1d φ1stKfuncH1stG=1stK1stH1stG
8 eqid BaseC=BaseC
9 8 1 2 cofu1st φ1stHfuncG=1stH1stG
10 9 coeq2d φ1stK1stHfuncG=1stK1stH1stG
11 4 7 10 3eqtr4a φ1stKfuncH1stG=1stK1stHfuncG
12 coass 1stH1stGx2ndK1stH1stGy1stGx2ndH1stGyx2ndGy=1stH1stGx2ndK1stH1stGy1stGx2ndH1stGyx2ndGy
13 2 3ad2ant1 φxBaseCyBaseCHDFuncE
14 3 3ad2ant1 φxBaseCyBaseCKEFuncF
15 relfunc RelCFuncD
16 1st2ndbr RelCFuncDGCFuncD1stGCFuncD2ndG
17 15 1 16 sylancr φ1stGCFuncD2ndG
18 17 3ad2ant1 φxBaseCyBaseC1stGCFuncD2ndG
19 8 5 18 funcf1 φxBaseCyBaseC1stG:BaseCBaseD
20 simp2 φxBaseCyBaseCxBaseC
21 19 20 ffvelrnd φxBaseCyBaseC1stGxBaseD
22 simp3 φxBaseCyBaseCyBaseC
23 19 22 ffvelrnd φxBaseCyBaseC1stGyBaseD
24 5 13 14 21 23 cofu2nd φxBaseCyBaseC1stGx2ndKfuncH1stGy=1stH1stGx2ndK1stH1stGy1stGx2ndH1stGy
25 24 coeq1d φxBaseCyBaseC1stGx2ndKfuncH1stGyx2ndGy=1stH1stGx2ndK1stH1stGy1stGx2ndH1stGyx2ndGy
26 1 3ad2ant1 φxBaseCyBaseCGCFuncD
27 8 26 13 20 cofu1 φxBaseCyBaseC1stHfuncGx=1stH1stGx
28 8 26 13 22 cofu1 φxBaseCyBaseC1stHfuncGy=1stH1stGy
29 27 28 oveq12d φxBaseCyBaseC1stHfuncGx2ndK1stHfuncGy=1stH1stGx2ndK1stH1stGy
30 8 26 13 20 22 cofu2nd φxBaseCyBaseCx2ndHfuncGy=1stGx2ndH1stGyx2ndGy
31 29 30 coeq12d φxBaseCyBaseC1stHfuncGx2ndK1stHfuncGyx2ndHfuncGy=1stH1stGx2ndK1stH1stGy1stGx2ndH1stGyx2ndGy
32 12 25 31 3eqtr4a φxBaseCyBaseC1stGx2ndKfuncH1stGyx2ndGy=1stHfuncGx2ndK1stHfuncGyx2ndHfuncGy
33 32 mpoeq3dva φxBaseC,yBaseC1stGx2ndKfuncH1stGyx2ndGy=xBaseC,yBaseC1stHfuncGx2ndK1stHfuncGyx2ndHfuncGy
34 11 33 opeq12d φ1stKfuncH1stGxBaseC,yBaseC1stGx2ndKfuncH1stGyx2ndGy=1stK1stHfuncGxBaseC,yBaseC1stHfuncGx2ndK1stHfuncGyx2ndHfuncGy
35 2 3 cofucl φKfuncHDFuncF
36 8 1 35 cofuval φKfuncHfuncG=1stKfuncH1stGxBaseC,yBaseC1stGx2ndKfuncH1stGyx2ndGy
37 1 2 cofucl φHfuncGCFuncE
38 8 37 3 cofuval φKfuncHfuncG=1stK1stHfuncGxBaseC,yBaseC1stHfuncGx2ndK1stHfuncGyx2ndHfuncGy
39 34 36 38 3eqtr4d φKfuncHfuncG=KfuncHfuncG