This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑉 )
Assertion lvecdim0 ( 𝑉 ∈ LVec → ( ( dim ‘ 𝑉 ) = 0 ↔ ( Base ‘ 𝑉 ) = { 0 } ) )

Proof

Step Hyp Ref Expression
1 lvecdim0.1 ⊢ 0 = ( 0g ‘ 𝑉 )
2 1 lvecdim0i ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ( Base ‘ 𝑉 ) = { 0 } )
3 simpl ⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → 𝑉 ∈ LVec )
4 eqid ⊢ ( LBasis ‘ 𝑉 ) = ( LBasis ‘ 𝑉 )
5 4 lbsex ⊢ ( 𝑉 ∈ LVec → ( LBasis ‘ 𝑉 ) ≠ ∅ )
6 n0 ⊢ ( ( LBasis ‘ 𝑉 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
7 5 6 sylib ⊢ ( 𝑉 ∈ LVec → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
8 3 7 syl ⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
9 1 fvexi ⊢ 0 ∈ V
10 9 snid ⊢ 0 ∈ { 0 }
11 simpr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑏 = { 0 } )
12 10 11 eleqtrrid ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 0 ∈ 𝑏 )
13 simplll ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑉 ∈ LVec )
14 4 lbslinds ⊢ ( LBasis ‘ 𝑉 ) ⊆ ( LIndS ‘ 𝑉 )
15 simplr ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
16 14 15 sselid ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑏 ∈ ( LIndS ‘ 𝑉 ) )
17 1 0nellinds ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑏 ∈ ( LIndS ‘ 𝑉 ) ) → ¬ 0 ∈ 𝑏 )
18 13 16 17 syl2anc ⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → ¬ 0 ∈ 𝑏 )
19 12 18 pm2.65da ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ¬ 𝑏 = { 0 } )
20 simpr ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
21 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
22 21 4 lbsss ⊢ ( 𝑏 ∈ ( LBasis ‘ 𝑉 ) → 𝑏 ⊆ ( Base ‘ 𝑉 ) )
23 20 22 syl ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ⊆ ( Base ‘ 𝑉 ) )
24 simplr ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( Base ‘ 𝑉 ) = { 0 } )
25 23 24 sseqtrd ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ⊆ { 0 } )
26 sssn ⊢ ( 𝑏 ⊆ { 0 } ↔ ( 𝑏 = ∅ ∨ 𝑏 = { 0 } ) )
27 25 26 sylib ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( 𝑏 = ∅ ∨ 𝑏 = { 0 } ) )
28 27 orcomd ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( 𝑏 = { 0 } ∨ 𝑏 = ∅ ) )
29 28 ord ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( ¬ 𝑏 = { 0 } → 𝑏 = ∅ ) )
30 19 29 mpd ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 = ∅ )
31 30 20 eqeltrrd ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ∅ ∈ ( LBasis ‘ 𝑉 ) )
32 8 31 exlimddv ⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ∅ ∈ ( LBasis ‘ 𝑉 ) )
33 4 dimval ⊢ ( ( 𝑉 ∈ LVec ∧ ∅ ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ ∅ ) )
34 3 32 33 syl2anc ⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ ∅ ) )
35 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
36 34 35 eqtrdi ⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ( dim ‘ 𝑉 ) = 0 )
37 2 36 impbida ⊢ ( 𝑉 ∈ LVec → ( ( dim ‘ 𝑉 ) = 0 ↔ ( Base ‘ 𝑉 ) = { 0 } ) )