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\mathrm{freeLMod}\left(0..^N\right)$$
	frlmfzowrd.b	$$⊢B={\mathrm{Base}}_W$$
	frlmfzowrd.s	$$⊢S={\mathrm{Base}}_K$$
Assertion	frlmfzolen	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in B\right)\to \left|X\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		frlmfzowrd.w	$$⊢W=K\mathrm{freeLMod}\left(0..^N\right)$$
2		frlmfzowrd.b	$$⊢B={\mathrm{Base}}_W$$
3		frlmfzowrd.s	$$⊢S={\mathrm{Base}}_K$$
4		ovexd	$$⊢N\in {\mathbb{N}}_0\to \left(0..^N\right)\in \mathrm{V}$$
5	1 3 2	frlmbasf	$$⊢\left(\left(0..^N\right)\in \mathrm{V}\wedge X\in B\right)\to X:\left(0..^N\right)⟶S$$
6	4 5	sylan	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in B\right)\to X:\left(0..^N\right)⟶S$$
7		fnfzo0hash	$$⊢\left(N\in {\mathbb{N}}_0\wedge X:\left(0..^N\right)⟶S\right)\to \left|X\right|=N$$
8	6 7	syldan	$$⊢\left(N\in {\mathbb{N}}_0\wedge X\in B\right)\to \left|X\right|=N$$