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

Metamath Proof Explorer

Theorem ablocom

Description: An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 ⊢ 𝑋 = ran 𝐺
Assertion ablocom ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ablcom.1 ⊢ 𝑋 = ran 𝐺
2 1 isablo ⊢ ( 𝐺 ∈ AbelOp ↔ ( 𝐺 ∈ GrpOp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )
3 2 simprbi ⊢ ( 𝐺 ∈ AbelOp → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) )
4 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑦 ) = ( 𝐴 𝐺 𝑦 ) )
5 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝐺 𝑥 ) = ( 𝑦 𝐺 𝐴 ) )
6 4 5 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ↔ ( 𝐴 𝐺 𝑦 ) = ( 𝑦 𝐺 𝐴 ) ) )
7 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
8 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝐺 𝐴 ) = ( 𝐵 𝐺 𝐴 ) )
9 7 8 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐺 𝑦 ) = ( 𝑦 𝐺 𝐴 ) ↔ ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) ) )
10 6 9 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) ) )
11 3 10 syl5com ⊢ ( 𝐺 ∈ AbelOp → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) ) )
12 11 3impib ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) )