Metamath Proof Explorer

Theorem lvecdim0i

Description: A vector space of dimension zero is reduced to its identity element. (Contributed by Thierry Arnoux, 31-Jul-2023)

Ref Expression
Hypothesis lvecdim0.1 
|- .0. = ( 0g ` V )
Assertion lvecdim0i 
|- ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> ( Base ` V ) = { .0. } )

Proof

Step Hyp Ref Expression
1 lvecdim0.1 
 |-  .0. = ( 0g ` V )
2 eqid 
 |-  ( LBasis ` V ) = ( LBasis ` V )
3 2 lbsex 
 |-  ( V e. LVec -> ( LBasis ` V ) =/= (/) )
4 n0 
 |-  ( ( LBasis ` V ) =/= (/) <-> E. b b e. ( LBasis ` V ) )
5 3 4 sylib 
 |-  ( V e. LVec -> E. b b e. ( LBasis ` V ) )
6 5 adantr 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> E. b b e. ( LBasis ` V ) )
7 simpr 
 |-  ( ( ( V e. LVec /\ ( dim ` V ) = 0 ) /\ b e. ( LBasis ` V ) ) -> b e. ( LBasis ` V ) )
8 2 dimval 
 |-  ( ( V e. LVec /\ b e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` b ) )
9 8 adantlr 
 |-  ( ( ( V e. LVec /\ ( dim ` V ) = 0 ) /\ b e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` b ) )
10 simplr 
 |-  ( ( ( V e. LVec /\ ( dim ` V ) = 0 ) /\ b e. ( LBasis ` V ) ) -> ( dim ` V ) = 0 )
11 9 10 eqtr3d 
 |-  ( ( ( V e. LVec /\ ( dim ` V ) = 0 ) /\ b e. ( LBasis ` V ) ) -> ( # ` b ) = 0 )
12 hasheq0 
 |-  ( b e. ( LBasis ` V ) -> ( ( # ` b ) = 0 <-> b = (/) ) )
13 12 biimpa 
 |-  ( ( b e. ( LBasis ` V ) /\ ( # ` b ) = 0 ) -> b = (/) )
14 7 11 13 syl2anc 
 |-  ( ( ( V e. LVec /\ ( dim ` V ) = 0 ) /\ b e. ( LBasis ` V ) ) -> b = (/) )
15 14 7 eqeltrrd 
 |-  ( ( ( V e. LVec /\ ( dim ` V ) = 0 ) /\ b e. ( LBasis ` V ) ) -> (/) e. ( LBasis ` V ) )
16 6 15 exlimddv 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> (/) e. ( LBasis ` V ) )
17 eqid 
 |-  ( Base ` V ) = ( Base ` V )
18 eqid 
 |-  ( LSpan ` V ) = ( LSpan ` V )
19 17 2 18 lbssp 
 |-  ( (/) e. ( LBasis ` V ) -> ( ( LSpan ` V ) ` (/) ) = ( Base ` V ) )
20 16 19 syl 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> ( ( LSpan ` V ) ` (/) ) = ( Base ` V ) )
21 lveclmod 
 |-  ( V e. LVec -> V e. LMod )
22 21 adantr 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> V e. LMod )
23 1 18 lsp0 
 |-  ( V e. LMod -> ( ( LSpan ` V ) ` (/) ) = { .0. } )
24 22 23 syl 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> ( ( LSpan ` V ) ` (/) ) = { .0. } )
25 20 24 eqtr3d 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> ( Base ` V ) = { .0. } )