Theorem frlmfzowrd

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

	Ref	Expression
Hypotheses	frlmfzowrd.w	|- W = ( K freeLMod ( 0 ..^ N ) )
	frlmfzowrd.b	|- B = ( Base ` W )
	frlmfzowrd.s	|- S = ( Base ` K )
Assertion	frlmfzowrd	|- ( X e. B -> X e. Word S )

Proof

Step	Hyp	Ref	Expression
1		frlmfzowrd.w	|- W = ( K freeLMod ( 0 ..^ N ) )
2		frlmfzowrd.b	|- B = ( Base ` W )
3		frlmfzowrd.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		iswrdi	|- ( X : ( 0 ..^ N ) --> S -> X e. Word S )
8	6 7	syl	|- ( X e. B -> X e. Word S )