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 eqtr4di ⊢ 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