Metamath Proof Explorer

Theorem isablo

Description: The predicate "is an Abelian (commutative) group operation." (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypothesis isabl.1 
|- X = ran G
Assertion isablo 
|- ( G e. AbelOp <-> ( G e. GrpOp /\ A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )

Proof

Step Hyp Ref Expression
1 isabl.1 
 |-  X = ran G
2 rneq 
 |-  ( g = G -> ran g = ran G )
3 2 1 eqtr4di 
 |-  ( g = G -> ran g = X )
4 raleq 
 |-  ( ran g = X -> ( A. y e. ran g ( x g y ) = ( y g x ) <-> A. y e. X ( x g y ) = ( y g x ) ) )
5 4 raleqbi1dv 
 |-  ( ran g = X -> ( A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) <-> A. x e. X A. y e. X ( x g y ) = ( y g x ) ) )
6 3 5 syl 
 |-  ( g = G -> ( A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) <-> A. x e. X A. y e. X ( x g y ) = ( y g x ) ) )
7 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
8 oveq 
 |-  ( g = G -> ( y g x ) = ( y G x ) )
9 7 8 eqeq12d 
 |-  ( g = G -> ( ( x g y ) = ( y g x ) <-> ( x G y ) = ( y G x ) ) )
10 9 2ralbidv 
 |-  ( g = G -> ( A. x e. X A. y e. X ( x g y ) = ( y g x ) <-> A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )
11 6 10 bitrd 
 |-  ( g = G -> ( A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) <-> A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )
12 df-ablo 
 |-  AbelOp = { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }
13 11 12 elrab2 
 |-  ( G e. AbelOp <-> ( G e. GrpOp /\ A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )