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 ⊢ V ∈ LVec → dim ⁡ V ∈ ℕ 0 *

Proof

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