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 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 ) ) )