Metamath Proof Explorer


Theorem drngdimgt0

Description: The dimension of a vector space that is also a division ring is greater than zero. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion drngdimgt0 F LVec F DivRing 0 < dim F

Proof

Step Hyp Ref Expression
1 1m1e0 1 1 = 0
2 simpl F LVec F DivRing F LVec
3 simpr F LVec F DivRing F DivRing
4 drngring F DivRing F Ring
5 eqid Base F = Base F
6 eqid 1 F = 1 F
7 5 6 ringidcl F Ring 1 F Base F
8 3 4 7 3syl F LVec F DivRing 1 F Base F
9 eqid 0 F = 0 F
10 9 6 drngunz F DivRing 1 F 0 F
11 10 adantl F LVec F DivRing 1 F 0 F
12 eqid LSpan F = LSpan F
13 eqid F 𝑠 LSpan F 1 F = F 𝑠 LSpan F 1 F
14 5 12 9 13 lsatdim F LVec 1 F Base F 1 F 0 F dim F 𝑠 LSpan F 1 F = 1
15 2 8 11 14 syl3anc F LVec F DivRing dim F 𝑠 LSpan F 1 F = 1
16 lveclmod F LVec F LMod
17 16 adantr F LVec F DivRing F LMod
18 8 snssd F LVec F DivRing 1 F Base F
19 eqid LSubSp F = LSubSp F
20 5 19 12 lspcl F LMod 1 F Base F LSpan F 1 F LSubSp F
21 17 18 20 syl2anc F LVec F DivRing LSpan F 1 F LSubSp F
22 13 lssdimle F LVec LSpan F 1 F LSubSp F dim F 𝑠 LSpan F 1 F dim F
23 2 21 22 syl2anc F LVec F DivRing dim F 𝑠 LSpan F 1 F dim F
24 15 23 eqbrtrrd F LVec F DivRing 1 dim F
25 1nn0 1 0
26 dimcl F LVec dim F 0 *
27 26 adantr F LVec F DivRing dim F 0 *
28 xnn0lem1lt 1 0 dim F 0 * 1 dim F 1 1 < dim F
29 25 27 28 sylancr F LVec F DivRing 1 dim F 1 1 < dim F
30 24 29 mpbid F LVec F DivRing 1 1 < dim F
31 1 30 eqbrtrrid F LVec F DivRing 0 < dim F