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

Theorem grpass 18108
Description: A group operation is associative. (Contributed by NM, 14-Aug-2011.)
Hypotheses
Ref Expression
grpcl.b 𝐵 = (Base‘𝐺)
grpcl.p + = (+g𝐺)
Assertion
Ref Expression
grpass ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))

Proof of Theorem grpass
StepHypRef Expression
1 grpmnd 18106 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpcl.p . . 3 + = (+g𝐺)
42, 3mndass 17916 . 2 ((𝐺 ∈ Mnd ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
51, 4sylan 583 1 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2112  cfv 6328  (class class class)co 7139  Basecbs 16479  +gcplusg 16561  Mndcmnd 17907  Grpcgrp 18099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-sgrp 17897  df-mnd 17908  df-grp 18102
This theorem is referenced by:  grprcan  18133  grprinv  18149  grpinvid1  18150  grpinvid2  18151  grplcan  18157  grpasscan1  18158  grpasscan2  18159  grplmulf1o  18169  grpinvadd  18173  grpsubadd  18183  grpaddsubass  18185  grpsubsub4  18188  dfgrp3  18194  grplactcnv  18198  imasgrp  18211  mulgaddcomlem  18246  mulgaddcom  18247  mulgdirlem  18254  issubg2  18290  isnsg3  18308  nmzsubg  18313  ssnmz  18314  eqger  18326  eqgcpbl  18330  qusgrp  18331  conjghm  18385  conjnmz  18388  subgga  18426  cntzsubg  18463  sylow1lem2  18720  sylow2blem1  18741  sylow2blem2  18742  sylow2blem3  18743  sylow3lem1  18748  sylow3lem2  18749  lsmass  18791  lsmmod  18797  lsmdisj2  18804  gex2abl  18968  ringcom  19329  lmodass  19646  evpmodpmf1o  20289  psrgrp  20640  ghmcnp  22724  qustgpopn  22729  cnncvsaddassdemo  23772  ogrpaddltbi  30773  ogrpaddltrbid  30775  ogrpinvlt  30778  cyc3genpmlem  30847  archiabllem2c  30878  lfladdass  36368  dvhvaddass  38392
  Copyright terms: Public domain W3C validator