Metamath Proof Explorer


Theorem mhmco

Description: The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Assertion mhmco FTMndHomUGSMndHomTFGSMndHomU

Proof

Step Hyp Ref Expression
1 mhmrcl2 FTMndHomUUMnd
2 mhmrcl1 GSMndHomTSMnd
3 1 2 anim12ci FTMndHomUGSMndHomTSMndUMnd
4 eqid BaseT=BaseT
5 eqid BaseU=BaseU
6 4 5 mhmf FTMndHomUF:BaseTBaseU
7 eqid BaseS=BaseS
8 7 4 mhmf GSMndHomTG:BaseSBaseT
9 fco F:BaseTBaseUG:BaseSBaseTFG:BaseSBaseU
10 6 8 9 syl2an FTMndHomUGSMndHomTFG:BaseSBaseU
11 eqid +S=+S
12 eqid +T=+T
13 7 11 12 mhmlin GSMndHomTxBaseSyBaseSGx+Sy=Gx+TGy
14 13 3expb GSMndHomTxBaseSyBaseSGx+Sy=Gx+TGy
15 14 adantll FTMndHomUGSMndHomTxBaseSyBaseSGx+Sy=Gx+TGy
16 15 fveq2d FTMndHomUGSMndHomTxBaseSyBaseSFGx+Sy=FGx+TGy
17 simpll FTMndHomUGSMndHomTxBaseSyBaseSFTMndHomU
18 8 ad2antlr FTMndHomUGSMndHomTxBaseSyBaseSG:BaseSBaseT
19 simprl FTMndHomUGSMndHomTxBaseSyBaseSxBaseS
20 18 19 ffvelcdmd FTMndHomUGSMndHomTxBaseSyBaseSGxBaseT
21 simprr FTMndHomUGSMndHomTxBaseSyBaseSyBaseS
22 18 21 ffvelcdmd FTMndHomUGSMndHomTxBaseSyBaseSGyBaseT
23 eqid +U=+U
24 4 12 23 mhmlin FTMndHomUGxBaseTGyBaseTFGx+TGy=FGx+UFGy
25 17 20 22 24 syl3anc FTMndHomUGSMndHomTxBaseSyBaseSFGx+TGy=FGx+UFGy
26 16 25 eqtrd FTMndHomUGSMndHomTxBaseSyBaseSFGx+Sy=FGx+UFGy
27 2 adantl FTMndHomUGSMndHomTSMnd
28 7 11 mndcl SMndxBaseSyBaseSx+SyBaseS
29 28 3expb SMndxBaseSyBaseSx+SyBaseS
30 27 29 sylan FTMndHomUGSMndHomTxBaseSyBaseSx+SyBaseS
31 fvco3 G:BaseSBaseTx+SyBaseSFGx+Sy=FGx+Sy
32 18 30 31 syl2anc FTMndHomUGSMndHomTxBaseSyBaseSFGx+Sy=FGx+Sy
33 fvco3 G:BaseSBaseTxBaseSFGx=FGx
34 18 19 33 syl2anc FTMndHomUGSMndHomTxBaseSyBaseSFGx=FGx
35 fvco3 G:BaseSBaseTyBaseSFGy=FGy
36 18 21 35 syl2anc FTMndHomUGSMndHomTxBaseSyBaseSFGy=FGy
37 34 36 oveq12d FTMndHomUGSMndHomTxBaseSyBaseSFGx+UFGy=FGx+UFGy
38 26 32 37 3eqtr4d FTMndHomUGSMndHomTxBaseSyBaseSFGx+Sy=FGx+UFGy
39 38 ralrimivva FTMndHomUGSMndHomTxBaseSyBaseSFGx+Sy=FGx+UFGy
40 8 adantl FTMndHomUGSMndHomTG:BaseSBaseT
41 eqid 0S=0S
42 7 41 mndidcl SMnd0SBaseS
43 27 42 syl FTMndHomUGSMndHomT0SBaseS
44 fvco3 G:BaseSBaseT0SBaseSFG0S=FG0S
45 40 43 44 syl2anc FTMndHomUGSMndHomTFG0S=FG0S
46 eqid 0T=0T
47 41 46 mhm0 GSMndHomTG0S=0T
48 47 adantl FTMndHomUGSMndHomTG0S=0T
49 48 fveq2d FTMndHomUGSMndHomTFG0S=F0T
50 eqid 0U=0U
51 46 50 mhm0 FTMndHomUF0T=0U
52 51 adantr FTMndHomUGSMndHomTF0T=0U
53 45 49 52 3eqtrd FTMndHomUGSMndHomTFG0S=0U
54 10 39 53 3jca FTMndHomUGSMndHomTFG:BaseSBaseUxBaseSyBaseSFGx+Sy=FGx+UFGyFG0S=0U
55 7 5 11 23 41 50 ismhm FGSMndHomUSMndUMndFG:BaseSBaseUxBaseSyBaseSFGx+Sy=FGx+UFGyFG0S=0U
56 3 54 55 sylanbrc FTMndHomUGSMndHomTFGSMndHomU