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	3	grpmndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6	1 2 5 4	iscmnd	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
7		isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
8	3 6 7	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ Abel )