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 | ||
frlmfzwrd.b | |||
frlmfzwrd.s | |||
Assertion | frlmfzwrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frlmfzwrd.w | ||
2 | frlmfzwrd.b | ||
3 | frlmfzwrd.s | ||
4 | ovex | ||
5 | 1 3 2 | frlmbasf | |
6 | 4 5 | mpan | |
7 | ffz0iswrd | ||
8 | 6 7 | syl |