Theorem circsubm

Description: The circle group T is a submonoid of the multiplicative group of CCfld . (Contributed by Thierry Arnoux, 26-Jan-2020)

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

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		ax-icn	|- _i e. CC
12	11	a1i	|- ( T. -> _i e. CC )
13		resubdrg	|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
14	13	simpli	|- RR e. ( SubRing ` CCfld )
15		subrgsubg	|- ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) )
16	14 15	ax-mp	|- RR e. ( SubGrp ` CCfld )
17	16	a1i	|- ( T. -> RR e. ( SubGrp ` CCfld ) )
18	5 10 12 17	efsubm	|- ( T. -> ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
19	18	mptru	|- ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) e. ( SubMnd ` ( mulGrp ` CCfld ) )
20	9 19	eqeltri	|- C e. ( SubMnd ` ( mulGrp ` CCfld ) )