This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isabl2

Description: The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses iscmn.b 
|- B = ( Base ` G )
iscmn.p 
|- .+ = ( +g ` G )
Assertion isabl2 
|- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )

Proof

Step Hyp Ref Expression
1 iscmn.b 
 |-  B = ( Base ` G )
2 iscmn.p 
 |-  .+ = ( +g ` G )
3 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
4 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
5 1 2 iscmn 
 |-  ( G e. CMnd <-> ( G e. Mnd /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
6 5 baib 
 |-  ( G e. Mnd -> ( G e. CMnd <-> A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
7 4 6 syl 
 |-  ( G e. Grp -> ( G e. CMnd <-> A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
8 7 pm5.32i 
 |-  ( ( G e. Grp /\ G e. CMnd ) <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
9 3 8 bitri 
 |-  ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )