Metamath Proof Explorer

Theorem cmodscexp

Description: The powers of _i belong to the scalar subring of a subcomplex module if _i belongs to the scalar subring . (Contributed by AV, 18-Oct-2021)

Ref Expression
Hypotheses cmodscexp.f 
|- F = ( Scalar ` W )
cmodscexp.k 
|- K = ( Base ` F )
Assertion cmodscexp 
|- ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> ( _i ^ N ) e. K )

Proof

Step Hyp Ref Expression
1 cmodscexp.f 
 |-  F = ( Scalar ` W )
2 cmodscexp.k 
 |-  K = ( Base ` F )
3 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( ( W e. CMod /\ _i e. K ) -> _i e. CC )
5 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 cnfldexp 
 |-  ( ( _i e. CC /\ N e. NN0 ) -> ( N ( .g ` ( mulGrp ` CCfld ) ) _i ) = ( _i ^ N ) )
7 4 5 6 syl2an 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> ( N ( .g ` ( mulGrp ` CCfld ) ) _i ) = ( _i ^ N ) )
8 1 2 clmsubrg 
 |-  ( W e. CMod -> K e. ( SubRing ` CCfld ) )
9 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
10 9 subrgsubm 
 |-  ( K e. ( SubRing ` CCfld ) -> K e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
11 8 10 syl 
 |-  ( W e. CMod -> K e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
12 11 ad2antrr 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> K e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
13 5 adantl 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> N e. NN0 )
14 simplr 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> _i e. K )
15 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
16 15 submmulgcl 
 |-  ( ( K e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ N e. NN0 /\ _i e. K ) -> ( N ( .g ` ( mulGrp ` CCfld ) ) _i ) e. K )
17 12 13 14 16 syl3anc 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> ( N ( .g ` ( mulGrp ` CCfld ) ) _i ) e. K )
18 7 17 eqeltrrd 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> ( _i ^ N ) e. K )