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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) )