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

Proof

Step Hyp Ref Expression
1 lvecdim0.1 ⊢0˙=0V
2 eqid ⊢LBasis⁡V=LBasis⁡V
3 2 lbsex ⊢V∈LVec→LBasis⁡V≠∅
4 n0 ⊢LBasis⁡V≠∅↔∃bb∈LBasis⁡V
5 3 4 sylib ⊢V∈LVec→∃bb∈LBasis⁡V
6 5 adantr ⊢V∈LVec∧dim⁡V=0→∃bb∈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 ⊢BaseV=BaseV
18 eqid ⊢LSpan⁡V=LSpan⁡V
19 17 2 18 lbssp ⊢∅∈LBasis⁡V→LSpan⁡V⁡∅=BaseV
20 16 19 syl ⊢V∈LVec∧dim⁡V=0→LSpan⁡V⁡∅=BaseV
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→BaseV=0˙