Metamath Proof Explorer


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 0 X 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 0 0 ..^ N V
5 1 3 2 frlmbasf 0 ..^ N V X B X : 0 ..^ N S
6 4 5 sylan N 0 X B X : 0 ..^ N S
7 fnfzo0hash N 0 X : 0 ..^ N S X = N
8 6 7 syldan N 0 X B X = N