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 ⊢BaseF=BaseF
6 eqid ⊢1F=1F
7 5 6 ringidcl ⊢F∈Ring→1F∈BaseF
8 3 4 7 3syl ⊢F∈LVec∧F∈DivRing→1F∈BaseF
9 eqid ⊢0F=0F
10 9 6 drngunz ⊢F∈DivRing→1F≠0F
11 10 adantl ⊢F∈LVec∧F∈DivRing→1F≠0F
12 eqid ⊢LSpan⁡F=LSpan⁡F
13 eqid ⊢F↾𝑠LSpan⁡F⁡1F=F↾𝑠LSpan⁡F⁡1F
14 5 12 9 13 lsatdim ⊢F∈LVec∧1F∈BaseF∧1F≠0F→dim⁡F↾𝑠LSpan⁡F⁡1F=1
15 2 8 11 14 syl3anc ⊢F∈LVec∧F∈DivRing→dim⁡F↾𝑠LSpan⁡F⁡1F=1
16 lveclmod ⊢F∈LVec→F∈LMod
17 16 adantr ⊢F∈LVec∧F∈DivRing→F∈LMod
18 8 snssd ⊢F∈LVec∧F∈DivRing→1F⊆BaseF
19 eqid ⊢LSubSp⁡F=LSubSp⁡F
20 5 19 12 lspcl ⊢F∈LMod∧1F⊆BaseF→LSpan⁡F⁡1F∈LSubSp⁡F
21 17 18 20 syl2anc ⊢F∈LVec∧F∈DivRing→LSpan⁡F⁡1F∈LSubSp⁡F
22 13 lssdimle ⊢F∈LVec∧LSpan⁡F⁡1F∈LSubSp⁡F→dim⁡F↾𝑠LSpan⁡F⁡1F≤dim⁡F
23 2 21 22 syl2anc ⊢F∈LVec∧F∈DivRing→dim⁡F↾𝑠LSpan⁡F⁡1F≤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