Theorem isabloi

Description: Properties that determine an Abelian group operation. (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isabli.1	⊢ 𝐺 ∈ GrpOp
	isabli.2	⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
	isabli.3	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) )
Assertion	isabloi	⊢ 𝐺 ∈ AbelOp

Proof

Step	Hyp	Ref	Expression
1		isabli.1	⊢ 𝐺 ∈ GrpOp
2		isabli.2	⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
3		isabli.3	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) )
4	3	rgen2	⊢ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
5	1 2	grporn	⊢ 𝑋 = ran 𝐺
6	5	isablo	⊢ ( 𝐺 ∈ AbelOp ↔ ( 𝐺 ∈ GrpOp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )
7	1 4 6	mpbir2an	⊢ 𝐺 ∈ AbelOp