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

Theorem grpass 18758
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 18756 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpcl.p . . 3 + = (+g𝐺)
42, 3mndass 18566 . 2 ((𝐺 ∈ Mnd ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
51, 4sylan 581 1 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  cfv 6497  (class class class)co 7358  Basecbs 17084  +gcplusg 17134  Mndcmnd 18557  Grpcgrp 18749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-sgrp 18547  df-mnd 18558  df-grp 18752
This theorem is referenced by:  grprcan  18785  grprinv  18802  grpinvid1  18803  grpinvid2  18804  grplcan  18810  grpasscan1  18811  grpasscan2  18812  grplmulf1o  18822  grpinvadd  18826  grpsubadd  18836  grpaddsubass  18838  grpsubsub4  18841  dfgrp3  18847  grplactcnv  18851  imasgrp  18864  mulgaddcomlem  18900  mulgaddcom  18901  mulgdirlem  18908  issubg2  18944  isnsg3  18963  nmzsubg  18968  ssnmz  18969  eqger  18981  eqgcpbl  18985  qusgrp  18986  conjghm  19040  conjnmz  19043  subgga  19081  cntzsubg  19118  sylow1lem2  19382  sylow2blem1  19403  sylow2blem2  19404  sylow2blem3  19405  sylow3lem1  19410  sylow3lem2  19411  lsmass  19452  lsmmod  19458  lsmdisj2  19465  gex2abl  19630  ringcom  20002  lmodass  20340  evpmodpmf1o  21003  psrgrpOLD  21370  ghmcnp  23469  qustgpopn  23474  cnncvsaddassdemo  24530  ogrpaddltbi  31929  ogrpaddltrbid  31931  ogrpinvlt  31934  cyc3genpmlem  32003  archiabllem2c  32034  quslsm  32189  lfladdass  37538  dvhvaddass  39563  grpassd  40687
  Copyright terms: Public domain W3C validator