This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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