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 e. LVec -> ( dim ` V ) e. NN0* )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( LBasis ` V ) = ( LBasis ` V )
2 1 lbsex 
 |-  ( V e. LVec -> ( LBasis ` V ) =/= (/) )
3 n0 
 |-  ( ( LBasis ` V ) =/= (/) <-> E. b b e. ( LBasis ` V ) )
4 2 3 sylib 
 |-  ( V e. LVec -> E. b b e. ( LBasis ` V ) )
5 1 dimval 
 |-  ( ( V e. LVec /\ b e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` b ) )
6 hashxnn0 
 |-  ( b e. ( LBasis ` V ) -> ( # ` b ) e. NN0* )
7 6 adantl 
 |-  ( ( V e. LVec /\ b e. ( LBasis ` V ) ) -> ( # ` b ) e. NN0* )
8 5 7 eqeltrd 
 |-  ( ( V e. LVec /\ b e. ( LBasis ` V ) ) -> ( dim ` V ) e. NN0* )
9 4 8 exlimddv 
 |-  ( V e. LVec -> ( dim ` V ) e. NN0* )