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∈XxGy=yGx

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→∀y∈ran⁡gxgy=ygx↔∀y∈Xxgy=ygx
5 4 raleqbi1dv ⊢ran⁡g=X→∀x∈ran⁡g∀y∈ran⁡gxgy=ygx↔∀x∈X∀y∈Xxgy=ygx
6 3 5 syl ⊢g=G→∀x∈ran⁡g∀y∈ran⁡gxgy=ygx↔∀x∈X∀y∈Xxgy=ygx
7 oveq ⊢g=G→xgy=xGy
8 oveq ⊢g=G→ygx=yGx
9 7 8 eqeq12d ⊢g=G→xgy=ygx↔xGy=yGx
10 9 2ralbidv ⊢g=G→∀x∈X∀y∈Xxgy=ygx↔∀x∈X∀y∈XxGy=yGx
11 6 10 bitrd ⊢g=G→∀x∈ran⁡g∀y∈ran⁡gxgy=ygx↔∀x∈X∀y∈XxGy=yGx
12 df-ablo ⊢AbelOp=g∈GrpOp|∀x∈ran⁡g∀y∈ran⁡gxgy=ygx
13 11 12 elrab2 ⊢G∈AbelOp↔G∈GrpOp∧∀x∈X∀y∈XxGy=yGx