Metamath Proof Explorer

Theorem lvecdim0

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

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

Proof

Step Hyp Ref Expression
1 lvecdim0.1 
 |-  .0. = ( 0g ` V )
2 1 lvecdim0i 
 |-  ( ( V e. LVec /\ ( dim ` V ) = 0 ) -> ( Base ` V ) = { .0. } )
3 simpl 
 |-  ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) -> V e. LVec )
4 eqid 
 |-  ( LBasis ` V ) = ( LBasis ` V )
5 4 lbsex 
 |-  ( V e. LVec -> ( LBasis ` V ) =/= (/) )
6 n0 
 |-  ( ( LBasis ` V ) =/= (/) <-> E. b b e. ( LBasis ` V ) )
7 5 6 sylib 
 |-  ( V e. LVec -> E. b b e. ( LBasis ` V ) )
8 3 7 syl 
 |-  ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) -> E. b b e. ( LBasis ` V ) )
9 1 fvexi 
 |-  .0. e. _V
10 9 snid 
 |-  .0. e. { .0. }
11 simpr 
 |-  ( ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) /\ b = { .0. } ) -> b = { .0. } )
12 10 11 eleqtrrid 
 |-  ( ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) /\ b = { .0. } ) -> .0. e. b )
13 simplll 
 |-  ( ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) /\ b = { .0. } ) -> V e. LVec )
14 4 lbslinds 
 |-  ( LBasis ` V ) C_ ( LIndS ` V )
15 simplr 
 |-  ( ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) /\ b = { .0. } ) -> b e. ( LBasis ` V ) )
16 14 15 sselid 
 |-  ( ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) /\ b = { .0. } ) -> b e. ( LIndS ` V ) )
17 1 0nellinds 
 |-  ( ( V e. LVec /\ b e. ( LIndS ` V ) ) -> -. .0. e. b )
18 13 16 17 syl2anc 
 |-  ( ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) /\ b = { .0. } ) -> -. .0. e. b )
19 12 18 pm2.65da 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> -. b = { .0. } )
20 simpr 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> b e. ( LBasis ` V ) )
21 eqid 
 |-  ( Base ` V ) = ( Base ` V )
22 21 4 lbsss 
 |-  ( b e. ( LBasis ` V ) -> b C_ ( Base ` V ) )
23 20 22 syl 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> b C_ ( Base ` V ) )
24 simplr 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> ( Base ` V ) = { .0. } )
25 23 24 sseqtrd 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> b C_ { .0. } )
26 sssn 
 |-  ( b C_ { .0. } <-> ( b = (/) \/ b = { .0. } ) )
27 25 26 sylib 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> ( b = (/) \/ b = { .0. } ) )
28 27 orcomd 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> ( b = { .0. } \/ b = (/) ) )
29 28 ord 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> ( -. b = { .0. } -> b = (/) ) )
30 19 29 mpd 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> b = (/) )
31 30 20 eqeltrrd 
 |-  ( ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) /\ b e. ( LBasis ` V ) ) -> (/) e. ( LBasis ` V ) )
32 8 31 exlimddv 
 |-  ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) -> (/) e. ( LBasis ` V ) )
33 4 dimval 
 |-  ( ( V e. LVec /\ (/) e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` (/) ) )
34 3 32 33 syl2anc 
 |-  ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) -> ( dim ` V ) = ( # ` (/) ) )
35 hash0 
 |-  ( # ` (/) ) = 0
36 34 35 eqtrdi 
 |-  ( ( V e. LVec /\ ( Base ` V ) = { .0. } ) -> ( dim ` V ) = 0 )
37 2 36 impbida 
 |-  ( V e. LVec -> ( ( dim ` V ) = 0 <-> ( Base ` V ) = { .0. } ) )