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 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
frlmfzwrd.b 𝐵 = ( Base ‘ 𝑊 )
frlmfzwrd.s 𝑆 = ( Base ‘ 𝐾 )
Assertion frlmfzwrd ( 𝑋𝐵𝑋 ∈ Word 𝑆 )

Proof

Step Hyp Ref Expression
1 frlmfzwrd.w 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
2 frlmfzwrd.b 𝐵 = ( Base ‘ 𝑊 )
3 frlmfzwrd.s 𝑆 = ( Base ‘ 𝐾 )
4 ovex ( 0 ... 𝑁 ) ∈ V
5 1 3 2 frlmbasf ( ( ( 0 ... 𝑁 ) ∈ V ∧ 𝑋𝐵 ) → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
6 4 5 mpan ( 𝑋𝐵𝑋 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
7 ffz0iswrd ( 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝑆𝑋 ∈ Word 𝑆 )
8 6 7 syl ( 𝑋𝐵𝑋 ∈ Word 𝑆 )