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