Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mhmco Structured version   Unicode version

Theorem mhmco 14762
 Description: The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
Assertion
Ref Expression
mhmco MndHom MndHom MndHom

Proof of Theorem mhmco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mhmrcl2 14742 . . 3 MndHom
2 mhmrcl1 14741 . . 3 MndHom
31, 2anim12ci 551 . 2 MndHom MndHom
4 eqid 2436 . . . . 5
5 eqid 2436 . . . . 5
64, 5mhmf 14743 . . . 4 MndHom
7 eqid 2436 . . . . 5
87, 4mhmf 14743 . . . 4 MndHom
9 fco 5600 . . . 4
106, 8, 9syl2an 464 . . 3 MndHom MndHom
11 eqid 2436 . . . . . . . . . 10
12 eqid 2436 . . . . . . . . . 10
137, 11, 12mhmlin 14745 . . . . . . . . 9 MndHom
14133expb 1154 . . . . . . . 8 MndHom
1514adantll 695 . . . . . . 7 MndHom MndHom
1615fveq2d 5732 . . . . . 6 MndHom MndHom
17 simpll 731 . . . . . . 7 MndHom MndHom MndHom
188ad2antlr 708 . . . . . . . 8 MndHom MndHom
19 simprl 733 . . . . . . . 8 MndHom MndHom
2018, 19ffvelrnd 5871 . . . . . . 7 MndHom MndHom
21 simprr 734 . . . . . . . 8 MndHom MndHom
2218, 21ffvelrnd 5871 . . . . . . 7 MndHom MndHom
23 eqid 2436 . . . . . . . 8
244, 12, 23mhmlin 14745 . . . . . . 7 MndHom
2517, 20, 22, 24syl3anc 1184 . . . . . 6 MndHom MndHom
2616, 25eqtrd 2468 . . . . 5 MndHom MndHom
272adantl 453 . . . . . . 7 MndHom MndHom
287, 11mndcl 14695 . . . . . . . 8
29283expb 1154 . . . . . . 7
3027, 29sylan 458 . . . . . 6 MndHom MndHom
31 fvco3 5800 . . . . . 6
3218, 30, 31syl2anc 643 . . . . 5 MndHom MndHom
33 fvco3 5800 . . . . . . 7
3418, 19, 33syl2anc 643 . . . . . 6 MndHom MndHom
35 fvco3 5800 . . . . . . 7
3618, 21, 35syl2anc 643 . . . . . 6 MndHom MndHom
3734, 36oveq12d 6099 . . . . 5 MndHom MndHom
3826, 32, 373eqtr4d 2478 . . . 4 MndHom MndHom
3938ralrimivva 2798 . . 3 MndHom MndHom
408adantl 453 . . . . 5 MndHom MndHom
41 eqid 2436 . . . . . . 7
427, 41mndidcl 14714 . . . . . 6
4327, 42syl 16 . . . . 5 MndHom MndHom
44 fvco3 5800 . . . . 5
4540, 43, 44syl2anc 643 . . . 4 MndHom MndHom
46 eqid 2436 . . . . . . 7
4741, 46mhm0 14746 . . . . . 6 MndHom
4847adantl 453 . . . . 5 MndHom MndHom
4948fveq2d 5732 . . . 4 MndHom MndHom
50 eqid 2436 . . . . . 6
5146, 50mhm0 14746 . . . . 5 MndHom
5251adantr 452 . . . 4 MndHom MndHom
5345, 49, 523eqtrd 2472 . . 3 MndHom MndHom
5410, 39, 533jca 1134 . 2 MndHom MndHom
557, 5, 11, 23, 41, 50ismhm 14740 . 2 MndHom
563, 54, 55sylanbrc 646 1 MndHom MndHom MndHom
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2705   ccom 4882  wf 5450  cfv 5454  (class class class)co 6081  cbs 13469   cplusg 13529  c0g 13723  cmnd 14684   MndHom cmhm 14736 This theorem is referenced by:  ghmco  15025  rhmco  15832  lgseisenlem4  21136 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-riota 6549  df-map 7020  df-0g 13727  df-mnd 14690  df-mhm 14738
 Copyright terms: Public domain W3C validator