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 | ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) ) | |
frlmfzowrd.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | ||
frlmfzowrd.s | ⊢ 𝑆 = ( Base ‘ 𝐾 ) | ||
Assertion | frlmfzolen | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ♯ ‘ 𝑋 ) = 𝑁 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frlmfzowrd.w | ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) ) | |
2 | frlmfzowrd.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
3 | frlmfzowrd.s | ⊢ 𝑆 = ( Base ‘ 𝐾 ) | |
4 | ovexd | ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ∈ V ) | |
5 | 1 3 2 | frlmbasf | ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ V ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 ) |
6 | 4 5 | sylan | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 ) |
7 | fnfzo0hash | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 ) → ( ♯ ‘ 𝑋 ) = 𝑁 ) | |
8 | 6 7 | syldan | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ♯ ‘ 𝑋 ) = 𝑁 ) |