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 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) )
frlmfzowrd.b 𝐵 = ( Base ‘ 𝑊 )
frlmfzowrd.s 𝑆 = ( Base ‘ 𝐾 )
Assertion frlmfzolen ( ( 𝑁 ∈ ℕ0𝑋𝐵 ) → ( ♯ ‘ 𝑋 ) = 𝑁 )

Proof

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𝑋𝐵 ) → ( ♯ ‘ 𝑋 ) = 𝑁 )