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

Proof

Step Hyp Ref Expression
1 lvecdim0.1 ⊢ 0 = ( 0g ‘ 𝑉 )
2 eqid ⊢ ( LBasis ‘ 𝑉 ) = ( LBasis ‘ 𝑉 )
3 2 lbsex ⊢ ( 𝑉 ∈ LVec → ( LBasis ‘ 𝑉 ) ≠ ∅ )
4 n0 ⊢ ( ( LBasis ‘ 𝑉 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
5 3 4 sylib ⊢ ( 𝑉 ∈ LVec → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
6 5 adantr ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
7 simpr ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
8 2 dimval ⊢ ( ( 𝑉 ∈ LVec ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ 𝑏 ) )
9 8 adantlr ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ 𝑏 ) )
10 simplr ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = 0 )
11 9 10 eqtr3d ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( ♯ ‘ 𝑏 ) = 0 )
12 hasheq0 ⊢ ( 𝑏 ∈ ( LBasis ‘ 𝑉 ) → ( ( ♯ ‘ 𝑏 ) = 0 ↔ 𝑏 = ∅ ) )
13 12 biimpa ⊢ ( ( 𝑏 ∈ ( LBasis ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑏 ) = 0 ) → 𝑏 = ∅ )
14 7 11 13 syl2anc ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 = ∅ )
15 14 7 eqeltrrd ⊢ ( ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ∅ ∈ ( LBasis ‘ 𝑉 ) )
16 6 15 exlimddv ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ∅ ∈ ( LBasis ‘ 𝑉 ) )
17 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
18 eqid ⊢ ( LSpan ‘ 𝑉 ) = ( LSpan ‘ 𝑉 )
19 17 2 18 lbssp ⊢ ( ∅ ∈ ( LBasis ‘ 𝑉 ) → ( ( LSpan ‘ 𝑉 ) ‘ ∅ ) = ( Base ‘ 𝑉 ) )
20 16 19 syl ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ( ( LSpan ‘ 𝑉 ) ‘ ∅ ) = ( Base ‘ 𝑉 ) )
21 lveclmod ⊢ ( 𝑉 ∈ LVec → 𝑉 ∈ LMod )
22 21 adantr ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → 𝑉 ∈ LMod )
23 1 18 lsp0 ⊢ ( 𝑉 ∈ LMod → ( ( LSpan ‘ 𝑉 ) ‘ ∅ ) = { 0 } )
24 22 23 syl ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ( ( LSpan ‘ 𝑉 ) ‘ ∅ ) = { 0 } )
25 20 24 eqtr3d ⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ( Base ‘ 𝑉 ) = { 0 } )