This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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