Metamath Proof Explorer

Theorem 2zrngaabl

Description: R is an (additive) abelian group. (Contributed by AV, 11-Feb-2020)

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
Assertion 2zrngaabl ⊢ R ∈ Abel

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 1 2 2zrngagrp ⊢ R ∈ Grp
4 1 2 2zrngacmnd ⊢ R ∈ CMnd
5 3 4 pm3.2i ⊢ R ∈ Grp ∧ R ∈ CMnd
6 isabl ⊢ R ∈ Abel ↔ R ∈ Grp ∧ R ∈ CMnd
7 5 6 mpbir ⊢ R ∈ Abel