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

Theorem grpass 14820
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 14818 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpcl.p . . 3  |-  .+  =  ( +g  `  G )
42, 3mndass 14697 . 2  |-  ( ( G  e.  Mnd  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .+  Y
)  .+  Z )  =  ( X  .+  ( Y  .+  Z ) ) )
51, 4sylan 459 1  |-  ( ( G  e.  Grp  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .+  Y
)  .+  Z )  =  ( X  .+  ( Y  .+  Z ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1726   ` cfv 5455  (class class class)co 6082   Basecbs 13470   +g cplusg 13530   Mndcmnd 14685   Grpcgrp 14686
This theorem is referenced by:  grprcan  14839  grprinv  14853  grpinvid1  14854  grpinvid2  14855  grplcan  14858  grplmulf1o  14866  grpinvadd  14868  grpsubadd  14877  grpaddsubass  14879  grpsubsub4  14882  grplactcnv  14888  mulgdirlem  14915  imasgrp  14935  issubg2  14960  isnsg3  14975  nmzsubg  14982  ssnmz  14983  eqger  14991  eqgcpbl  14995  divsgrp  14996  conjghm  15037  conjnmz  15040  subgga  15078  cntzsubg  15136  sylow1lem2  15234  sylow2blem1  15255  sylow2blem2  15256  sylow2blem3  15257  sylow3lem1  15262  sylow3lem2  15263  lsmass  15303  lsmmod  15308  lsmdisj2  15315  gex2abl  15467  rngcom  15693  lmodass  15966  psrgrp  16463  ghmcnp  18145  divstgpopn  18150  lfladdass  29872  dvhvaddass  31896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-nul 4339  ax-pow 4378
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-sbc 3163  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-iota 5419  df-fv 5463  df-ov 6085  df-mnd 14691  df-grp 14813
  Copyright terms: Public domain W3C validator