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 ˙ = 0 V
Assertion lvecdim0i ⊢ V ∈ LVec ∧ dim ⁡ V = 0 → Base V = 0 ˙

Proof

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