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

Theorem mndass 16498
Description: A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)
Hypotheses
Ref Expression
mndcl.b  |-  B  =  ( Base `  G
)
mndcl.p  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
mndass  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .+  Y
)  .+  Z )  =  ( X  .+  ( Y  .+  Z ) ) )

Proof of Theorem mndass
StepHypRef Expression
1 mndsgrp 16495 . 2  |-  ( G  e.  Mnd  ->  G  e. SGrp )
2 mndcl.b . . 3  |-  B  =  ( Base `  G
)
3 mndcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3sgrpass 16485 . 2  |-  ( ( G  e. SGrp  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B )
)  ->  ( ( X  .+  Y )  .+  Z )  =  ( X  .+  ( Y 
.+  Z ) ) )
51, 4sylan 473 1  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .+  Y
)  .+  Z )  =  ( X  .+  ( Y  .+  Z ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867   ` cfv 5592  (class class class)co 6296   Basecbs 15081   +g cplusg 15150  SGrpcsgrp 16478   Mndcmnd 16487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-nul 4547
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-iota 5556  df-fv 5600  df-ov 6299  df-sgrp 16479  df-mnd 16489
This theorem is referenced by:  mnd32g  16503  mnd12g  16504  mnd4g  16505  issubmnd  16516  prdsmndd  16521  imasmnd  16526  mrcmndind  16565  gsumccat  16577  grpass  16632  mulgnndir  16732  mhmmnd  16760  cntzsubm  16941  oppgmnd  16957  frgp0  17351  mulgnn0di  17407  gsumval3eu  17479  gsumval3  17482  srgass  17688  ringass  17738  mndvass  19354  chfacfscmulgsum  19821  chfacfpmmulgsum  19825  slmdass  28408  lidlmsgrp  38741  invginvrid  38969
  Copyright terms: Public domain W3C validator