This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dimcl

Description: Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023)

Ref Expression
Assertion dimcl ( 𝑉 ∈ LVec → ( dim ‘ 𝑉 ) ∈ ℕ0* )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( LBasis ‘ 𝑉 ) = ( LBasis ‘ 𝑉 )
2 1 lbsex ⊢ ( 𝑉 ∈ LVec → ( LBasis ‘ 𝑉 ) ≠ ∅ )
3 n0 ⊢ ( ( LBasis ‘ 𝑉 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
4 2 3 sylib ⊢ ( 𝑉 ∈ LVec → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
5 1 dimval ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ 𝑏 ) )
6 hashxnn0 ⊢ ( 𝑏 ∈ ( LBasis ‘ 𝑉 ) → ( ♯ ‘ 𝑏 ) ∈ ℕ0* )
7 6 adantl ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( ♯ ‘ 𝑏 ) ∈ ℕ0* )
8 5 7 eqeltrd ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) ∈ ℕ0* )
9 4 8 exlimddv ⊢ ( 𝑉 ∈ LVec → ( dim ‘ 𝑉 ) ∈ ℕ0* )