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

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