Theorem 2zrngaabl

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

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion	2zrngaabl	⊢ 𝑅 ∈ Abel

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3	1 2	2zrngagrp	⊢ 𝑅 ∈ Grp
4	1 2	2zrngacmnd	⊢ 𝑅 ∈ CMnd
5	3 4	pm3.2i	⊢ ( 𝑅 ∈ Grp ∧ 𝑅 ∈ CMnd )
6		isabl	⊢ ( 𝑅 ∈ Abel ↔ ( 𝑅 ∈ Grp ∧ 𝑅 ∈ CMnd ) )
7	5 6	mpbir	⊢ 𝑅 ∈ Abel