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

Metamath Proof Explorer

Theorem cmodscmulexp

Description: The scalar product of a vector with powers of _i belongs to the base set of a subcomplex module if the scalar subring of th subcomplex module contains _i . (Contributed by AV, 18-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 cmodscexp.f 
 |-  F = ( Scalar ` W )
2 cmodscexp.k 
 |-  K = ( Base ` F )
3 cmodscmulexp.x 
 |-  X = ( Base ` W )
4 cmodscmulexp.s 
 |-  .x. = ( .s ` W )
5 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
6 5 adantr 
 |-  ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> W e. LMod )
7 simp1 
 |-  ( ( _i e. K /\ B e. X /\ N e. NN ) -> _i e. K )
8 7 anim2i 
 |-  ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> ( W e. CMod /\ _i e. K ) )
9 simpr3 
 |-  ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> N e. NN )
10 1 2 cmodscexp 
 |-  ( ( ( W e. CMod /\ _i e. K ) /\ N e. NN ) -> ( _i ^ N ) e. K )
11 8 9 10 syl2anc 
 |-  ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> ( _i ^ N ) e. K )
12 simpr2 
 |-  ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> B e. X )
13 3 1 4 2 lmodvscl 
 |-  ( ( W e. LMod /\ ( _i ^ N ) e. K /\ B e. X ) -> ( ( _i ^ N ) .x. B ) e. X )
14 6 11 12 13 syl3anc 
 |-  ( ( W e. CMod /\ ( _i e. K /\ B e. X /\ N e. NN ) ) -> ( ( _i ^ N ) .x. B ) e. X )