Theorem circgrp

Description: The circle group T is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008) (Revised by Mario Carneiro, 13-May-2014) (Revised by Thierry Arnoux, 26-Jan-2020)

	Ref	Expression
Hypotheses	circgrp.1	|- C = ( `' abs " { 1 } )
	circgrp.2	|- T = ( ( mulGrp ` CCfld ) |`s C )
Assertion	circgrp	|- T e. Abel

Proof

Step	Hyp	Ref	Expression
1		circgrp.1	|- C = ( `' abs " { 1 } )
2		circgrp.2	|- T = ( ( mulGrp ` CCfld ) |`s C )
3		oveq2	|- ( x = y -> ( _i x. x ) = ( _i x. y ) )
4	3	fveq2d	|- ( x = y -> ( exp ` ( _i x. x ) ) = ( exp ` ( _i x. y ) ) )
5	4	cbvmptv	|- ( x e. RR |-> ( exp ` ( _i x. x ) ) ) = ( y e. RR |-> ( exp ` ( _i x. y ) ) )
6	5 1	efifo	|- ( x e. RR |-> ( exp ` ( _i x. x ) ) ) : RR -onto-> C
7		forn	|- ( ( x e. RR |-> ( exp ` ( _i x. x ) ) ) : RR -onto-> C -> ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) = C )
8	6 7	ax-mp	|- ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) = C
9	8	eqcomi	|- C = ran ( x e. RR |-> ( exp ` ( _i x. x ) ) )
10	9	oveq2i	|- ( ( mulGrp ` CCfld ) |`s C ) = ( ( mulGrp ` CCfld ) |`s ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) )
11	2 10	eqtri	|- T = ( ( mulGrp ` CCfld ) |`s ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) )
12		ax-icn	|- _i e. CC
13	12	a1i	|- ( T. -> _i e. CC )
14		resubdrg	|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
15	14	simpli	|- RR e. ( SubRing ` CCfld )
16		subrgsubg	|- ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) )
17	15 16	ax-mp	|- RR e. ( SubGrp ` CCfld )
18	17	a1i	|- ( T. -> RR e. ( SubGrp ` CCfld ) )
19	5 11 13 18	efabl	|- ( T. -> T e. Abel )
20	19	mptru	|- T e. Abel