Theorem isabl2

Description: The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	iscmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscmn.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	isabl2	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscmn.p	⊢ + = ( +g ‘ 𝐺 )
3		isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
4		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
5	1 2	iscmn	⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
6	5	baib	⊢ ( 𝐺 ∈ Mnd → ( 𝐺 ∈ CMnd ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
7	4 6	syl	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ∈ CMnd ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
8	7	pm5.32i	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
9	3 8	bitri	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )