Metamath Proof Explorer

Theorem isass

Description: The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009) (New usage is discouraged.)

Ref Expression
Hypothesis isass.1 
|- X = dom dom G
Assertion isass 
|- ( G e. A -> ( G e. Ass <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )

Proof

Step Hyp Ref Expression
1 isass.1 
 |-  X = dom dom G
2 dmeq 
 |-  ( g = G -> dom g = dom G )
3 2 dmeqd 
 |-  ( g = G -> dom dom g = dom dom G )
4 3 eleq2d 
 |-  ( g = G -> ( x e. dom dom g <-> x e. dom dom G ) )
5 3 eleq2d 
 |-  ( g = G -> ( y e. dom dom g <-> y e. dom dom G ) )
6 3 eleq2d 
 |-  ( g = G -> ( z e. dom dom g <-> z e. dom dom G ) )
7 4 5 6 3anbi123d 
 |-  ( g = G -> ( ( x e. dom dom g /\ y e. dom dom g /\ z e. dom dom g ) <-> ( x e. dom dom G /\ y e. dom dom G /\ z e. dom dom G ) ) )
8 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
9 8 oveq1d 
 |-  ( g = G -> ( ( x g y ) g z ) = ( ( x G y ) g z ) )
10 oveq 
 |-  ( g = G -> ( ( x G y ) g z ) = ( ( x G y ) G z ) )
11 9 10 eqtrd 
 |-  ( g = G -> ( ( x g y ) g z ) = ( ( x G y ) G z ) )
12 oveq 
 |-  ( g = G -> ( y g z ) = ( y G z ) )
13 12 oveq2d 
 |-  ( g = G -> ( x g ( y g z ) ) = ( x g ( y G z ) ) )
14 oveq 
 |-  ( g = G -> ( x g ( y G z ) ) = ( x G ( y G z ) ) )
15 13 14 eqtrd 
 |-  ( g = G -> ( x g ( y g z ) ) = ( x G ( y G z ) ) )
16 11 15 eqeq12d 
 |-  ( g = G -> ( ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
17 7 16 imbi12d 
 |-  ( g = G -> ( ( ( x e. dom dom g /\ y e. dom dom g /\ z e. dom dom g ) -> ( ( x g y ) g z ) = ( x g ( y g z ) ) ) <-> ( ( x e. dom dom G /\ y e. dom dom G /\ z e. dom dom G ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
18 17 albidv 
 |-  ( g = G -> ( A. z ( ( x e. dom dom g /\ y e. dom dom g /\ z e. dom dom g ) -> ( ( x g y ) g z ) = ( x g ( y g z ) ) ) <-> A. z ( ( x e. dom dom G /\ y e. dom dom G /\ z e. dom dom G ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
19 18 2albidv 
 |-  ( g = G -> ( A. x A. y A. z ( ( x e. dom dom g /\ y e. dom dom g /\ z e. dom dom g ) -> ( ( x g y ) g z ) = ( x g ( y g z ) ) ) <-> A. x A. y A. z ( ( x e. dom dom G /\ y e. dom dom G /\ z e. dom dom G ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
20 r3al 
 |-  ( A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> A. x A. y A. z ( ( x e. dom dom g /\ y e. dom dom g /\ z e. dom dom g ) -> ( ( x g y ) g z ) = ( x g ( y g z ) ) ) )
21 r3al 
 |-  ( A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. x A. y A. z ( ( x e. dom dom G /\ y e. dom dom G /\ z e. dom dom G ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
22 19 20 21 3bitr4g 
 |-  ( g = G -> ( A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
23 1 eqcomi 
 |-  dom dom G = X
24 23 a1i 
 |-  ( g = G -> dom dom G = X )
25 24 raleqdv 
 |-  ( g = G -> ( A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. y e. X A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
26 24 25 raleqbidv 
 |-  ( g = G -> ( A. x e. dom dom G A. y e. dom dom G A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. x e. X A. y e. X A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
27 24 raleqdv 
 |-  ( g = G -> ( A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
28 27 2ralbidv 
 |-  ( g = G -> ( A. x e. X A. y e. X A. z e. dom dom G ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
29 22 26 28 3bitrd 
 |-  ( g = G -> ( A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
30 df-ass 
 |-  Ass = { g | A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) }
31 29 30 elab2g 
 |-  ( G e. A -> ( G e. Ass <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )