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* )