Theorem isabld

Description: Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013)

	Ref	Expression
Hypotheses	isabld.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	isabld.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
	isabld.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	isabld.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
Assertion	isabld	⊢ ( 𝜑 → 𝐺 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		isabld.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		isabld.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		isabld.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		isabld.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
5		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
6	3 5	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
7	1 2 6 4	iscmnd	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
8		isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
9	3 7 8	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ Abel )