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

Theorem grpoass 21748
Description: A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
Hypothesis
Ref Expression
grpfo.1  |-  X  =  ran  G
Assertion
Ref Expression
grpoass  |-  ( ( G  e.  GrpOp  /\  ( A  e.  X  /\  B  e.  X  /\  C  e.  X )
)  ->  ( ( A G B ) G C )  =  ( A G ( B G C ) ) )

Proof of Theorem grpoass
Dummy variables  x  y  z  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grpfo.1 . . . . 5  |-  X  =  ran  G
21isgrpo 21741 . . . 4  |-  ( G  e.  GrpOp  ->  ( G  e.  GrpOp 
<->  ( G : ( X  X.  X ) --> X  /\  A. x  e.  X  A. y  e.  X  A. z  e.  X  ( (
x G y ) G z )  =  ( x G ( y G z ) )  /\  E. u  e.  X  A. x  e.  X  ( (
u G x )  =  x  /\  E. y  e.  X  (
y G x )  =  u ) ) ) )
32ibi 233 . . 3  |-  ( G  e.  GrpOp  ->  ( G : ( X  X.  X ) --> X  /\  A. x  e.  X  A. y  e.  X  A. z  e.  X  (
( x G y ) G z )  =  ( x G ( y G z ) )  /\  E. u  e.  X  A. x  e.  X  (
( u G x )  =  x  /\  E. y  e.  X  ( y G x )  =  u ) ) )
43simp2d 970 . 2  |-  ( G  e.  GrpOp  ->  A. x  e.  X  A. y  e.  X  A. z  e.  X  ( (
x G y ) G z )  =  ( x G ( y G z ) ) )
5 oveq1 6051 . . . . 5  |-  ( x  =  A  ->  (
x G y )  =  ( A G y ) )
65oveq1d 6059 . . . 4  |-  ( x  =  A  ->  (
( x G y ) G z )  =  ( ( A G y ) G z ) )
7 oveq1 6051 . . . 4  |-  ( x  =  A  ->  (
x G ( y G z ) )  =  ( A G ( y G z ) ) )
86, 7eqeq12d 2422 . . 3  |-  ( x  =  A  ->  (
( ( x G y ) G z )  =  ( x G ( y G z ) )  <->  ( ( A G y ) G z )  =  ( A G ( y G z ) ) ) )
9 oveq2 6052 . . . . 5  |-  ( y  =  B  ->  ( A G y )  =  ( A G B ) )
109oveq1d 6059 . . . 4  |-  ( y  =  B  ->  (
( A G y ) G z )  =  ( ( A G B ) G z ) )
11 oveq1 6051 . . . . 5  |-  ( y  =  B  ->  (
y G z )  =  ( B G z ) )
1211oveq2d 6060 . . . 4  |-  ( y  =  B  ->  ( A G ( y G z ) )  =  ( A G ( B G z ) ) )
1310, 12eqeq12d 2422 . . 3  |-  ( y  =  B  ->  (
( ( A G y ) G z )  =  ( A G ( y G z ) )  <->  ( ( A G B ) G z )  =  ( A G ( B G z ) ) ) )
14 oveq2 6052 . . . 4  |-  ( z  =  C  ->  (
( A G B ) G z )  =  ( ( A G B ) G C ) )
15 oveq2 6052 . . . . 5  |-  ( z  =  C  ->  ( B G z )  =  ( B G C ) )
1615oveq2d 6060 . . . 4  |-  ( z  =  C  ->  ( A G ( B G z ) )  =  ( A G ( B G C ) ) )
1714, 16eqeq12d 2422 . . 3  |-  ( z  =  C  ->  (
( ( A G B ) G z )  =  ( A G ( B G z ) )  <->  ( ( A G B ) G C )  =  ( A G ( B G C ) ) ) )
188, 13, 17rspc3v 3025 . 2  |-  ( ( A  e.  X  /\  B  e.  X  /\  C  e.  X )  ->  ( A. x  e.  X  A. y  e.  X  A. z  e.  X  ( ( x G y ) G z )  =  ( x G ( y G z ) )  ->  ( ( A G B ) G C )  =  ( A G ( B G C ) ) ) )
194, 18mpan9 456 1  |-  ( ( G  e.  GrpOp  /\  ( A  e.  X  /\  B  e.  X  /\  C  e.  X )
)  ->  ( ( A G B ) G C )  =  ( A G ( B G C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2670   E.wrex 2671    X. cxp 4839   ran crn 4842   -->wf 5413  (class class class)co 6044   GrpOpcgr 21731
This theorem is referenced by:  grpoidinvlem1  21749  grpoidinvlem2  21750  grpoidinvlem4  21752  grporcan  21766  grpoinvid1  21775  grpoinvid2  21776  grpolcan  21778  grpo2grp  21779  grpoasscan1  21782  grpoasscan2  21783  grpoinvop  21786  grpomuldivass  21794  grponpcan  21797  grpopnpcan2  21798  gxcom  21814  gxnn0add  21819  ablo32  21831  ablo4  21832  issubgoi  21855  ghgrp  21913  rngoaass  21938  vcaass  21997  vcm  22007  nvass  22058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-fo 5423  df-fv 5425  df-ov 6047  df-grpo 21736
  Copyright terms: Public domain W3C validator