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 e. B -> X e. 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 ) e. _V
5	1 3 2	frlmbasf	|- ( ( ( 0 ... N ) e. _V /\ X e. B ) -> X : ( 0 ... N ) --> S )
6	4 5	mpan	|- ( X e. B -> X : ( 0 ... N ) --> S )
7		ffz0iswrd	|- ( X : ( 0 ... N ) --> S -> X e. Word S )
8	6 7	syl	|- ( X e. B -> X e. Word S )