Metamath Proof Explorer


Theorem frlmfzwrd

Description: A vector of a module with indices from 0 to N is a word over the scalars of the module. (Contributed by SN, 31-Aug-2023)

Ref Expression
Hypotheses frlmfzwrd.w W = K freeLMod 0 N
frlmfzwrd.b B = Base W
frlmfzwrd.s S = Base K
Assertion frlmfzwrd X B X Word S

Proof

Step Hyp Ref Expression
1 frlmfzwrd.w W = K freeLMod 0 N
2 frlmfzwrd.b B = Base W
3 frlmfzwrd.s S = Base K
4 ovex 0 N V
5 1 3 2 frlmbasf 0 N V X B X : 0 N S
6 4 5 mpan X B X : 0 N S
7 ffz0iswrd X : 0 N S X Word S
8 6 7 syl X B X Word S