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 AbelOp G GrpOp x X y 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 syl6eqr g = G ran g = X
4 raleq ran g = X y ran g x g y = y g x y X x g y = y g x
5 4 raleqbi1dv ran g = X x ran g y ran g x g y = y g x x X y X x g y = y g x
6 3 5 syl g = G x ran g y ran g x g y = y g x x X y 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 x X y X x g y = y g x x X y X x G y = y G x
11 6 10 bitrd g = G x ran g y ran g x g y = y g x x X y X x G y = y G x
12 df-ablo AbelOp = g GrpOp | x ran g y ran g x g y = y g x
13 11 12 elrab2 G AbelOp G GrpOp x X y X x G y = y G x