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

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 ⊢ 𝑋 = ran 𝐺
Assertion isablo ( 𝐺 ∈ AbelOp ↔ ( 𝐺 ∈ GrpOp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 isabl.1 ⊢ 𝑋 = ran 𝐺
2 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
3 2 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
4 raleq ⊢ ( ran 𝑔 = 𝑋 → ( ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ) )
5 4 raleqbi1dv ⊢ ( ran 𝑔 = 𝑋 → ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ) )
6 3 5 syl ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ) )
7 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
8 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
9 7 8 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ↔ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )
10 9 2ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )
11 6 10 bitrd ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )
12 df-ablo ⊢ AbelOp = { 𝑔 ∈ GrpOp ∣ ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( 𝑥 𝑔 𝑦 ) = ( 𝑦 𝑔 𝑥 ) }
13 11 12 elrab2 ⊢ ( 𝐺 ∈ AbelOp ↔ ( 𝐺 ∈ GrpOp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )