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 )