Metamath Proof Explorer


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