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

Theorem grpass 15573
Description: A group operation is associative. (Contributed by NM, 14-Aug-2011.)
Hypotheses
Ref Expression
grpcl.b  |-  B  =  ( Base `  G
)
grpcl.p  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
grpass  |-  ( ( G  e.  Grp  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .+  Y
)  .+  Z )  =  ( X  .+  ( Y  .+  Z ) ) )

Proof of Theorem grpass
StepHypRef Expression
1 grpmnd 15571 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndass 15442 . 2  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .+  Y
)  .+  Z )  =  ( X  .+  ( Y  .+  Z ) ) )
51, 4sylan 471 1  |-  ( ( G  e.  Grp  /\  ( 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 369    /\ w3a 965    = wceq 1369    e. wcel 1756   ` cfv 5439  (class class class)co 6112   Basecbs 14195   +g cplusg 14259   Mndcmnd 15430   Grpcgrp 15431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4442  ax-pow 4491
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-ov 6115  df-mnd 15436  df-grp 15566
This theorem is referenced by:  grprcan  15592  grprinv  15606  grpinvid1  15607  grpinvid2  15608  grplcan  15611  grplmulf1o  15621  grpinvadd  15625  grpsubadd  15634  grpaddsubass  15636  grpsubsub4  15639  grplactcnv  15645  mulgdirlem  15672  imasgrp  15692  issubg2  15717  isnsg3  15736  nmzsubg  15743  ssnmz  15744  eqger  15752  eqgcpbl  15756  divsgrp  15757  conjghm  15798  conjnmz  15801  subgga  15839  cntzsubg  15875  sylow1lem2  16119  sylow2blem1  16140  sylow2blem2  16141  sylow2blem3  16142  sylow3lem1  16147  sylow3lem2  16148  lsmass  16188  lsmmod  16193  lsmdisj2  16200  gex2abl  16354  rngcom  16695  lmodass  16985  psrgrp  17491  evpmodpmf1o  18048  ghmcnp  19707  divstgpopn  19712  ogrpaddltbi  26204  ogrpaddltrbid  26206  ogrpinvlt  26209  archiabllem2c  26234  lfladdass  32814  dvhvaddass  34838
  Copyright terms: Public domain W3C validator