Theorem frlmfzolen

Description: The dimension of a vector of a module with indices from 0 to N - 1 . (Contributed by SN, 1-Sep-2023)

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

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		ovexd	|- ( N e. NN0 -> ( 0 ..^ N ) e. _V )
5	1 3 2	frlmbasf	|- ( ( ( 0 ..^ N ) e. _V /\ X e. B ) -> X : ( 0 ..^ N ) --> S )
6	4 5	sylan	|- ( ( N e. NN0 /\ X e. B ) -> X : ( 0 ..^ N ) --> S )
7		fnfzo0hash	|- ( ( N e. NN0 /\ X : ( 0 ..^ N ) --> S ) -> ( # ` X ) = N )
8	6 7	syldan	|- ( ( N e. NN0 /\ X e. B ) -> ( # ` X ) = N )