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=ScalarW
cmodscexp.k K=BaseF
cmodscmulexp.x X=BaseW
cmodscmulexp.s ·˙=W
Assertion cmodscmulexp WCModiKBXNiN·˙BX

Proof

Step Hyp Ref Expression
1 cmodscexp.f F=ScalarW
2 cmodscexp.k K=BaseF
3 cmodscmulexp.x X=BaseW
4 cmodscmulexp.s ·˙=W
5 clmlmod WCModWLMod
6 5 adantr WCModiKBXNWLMod
7 simp1 iKBXNiK
8 7 anim2i WCModiKBXNWCModiK
9 simpr3 WCModiKBXNN
10 1 2 cmodscexp WCModiKNiNK
11 8 9 10 syl2anc WCModiKBXNiNK
12 simpr2 WCModiKBXNBX
13 3 1 4 2 lmodvscl WLModiNKBXiN·˙BX
14 6 11 12 13 syl3anc WCModiKBXNiN·˙BX