Theorem 2zrngaabl

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

	Ref	Expression
Hypotheses	2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
	2zrngbas.r	|- R = ( CCfld |`s E )
Assertion	2zrngaabl	|- R e. Abel

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2		2zrngbas.r	|- R = ( CCfld |`s E )
3	1 2	2zrngagrp	|- R e. Grp
4	1 2	2zrngacmnd	|- R e. CMnd
5	3 4	pm3.2i	|- ( R e. Grp /\ R e. CMnd )
6		isabl	|- ( R e. Abel <-> ( R e. Grp /\ R e. CMnd ) )
7	5 6	mpbir	|- R e. Abel