Metamath Proof Explorer

Theorem rlmdim

Description: The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023) Generalize to division rings. (Revised by SN, 22-Mar-2025)

Ref Expression
Hypothesis rlmdim.1 ⊢ V = ringLMod ⁡ F
Assertion rlmdim ⊢ F ∈ DivRing → dim ⁡ V = 1

Proof

Step Hyp Ref Expression
1 rlmdim.1 ⊢ V = ringLMod ⁡ F
2 rlmlvec ⊢ F ∈ DivRing → ringLMod ⁡ F ∈ LVec
3 1 2 eqeltrid ⊢ F ∈ DivRing → V ∈ LVec
4 ssid ⊢ Base F ⊆ Base F
5 rlmval ⊢ ringLMod ⁡ F = subringAlg ⁡ F ⁡ Base F
6 1 5 eqtri ⊢ V = subringAlg ⁡ F ⁡ Base F
7 eqid ⊢ Base F = Base F
8 6 7 sradrng ⊢ F ∈ DivRing ∧ Base F ⊆ Base F → V ∈ DivRing
9 4 8 mpan2 ⊢ F ∈ DivRing → V ∈ DivRing
10 9 drngringd ⊢ F ∈ DivRing → V ∈ Ring
11 eqid ⊢ Base V = Base V
12 eqid ⊢ 1 V = 1 V
13 11 12 ringidcl ⊢ V ∈ Ring → 1 V ∈ Base V
14 10 13 syl ⊢ F ∈ DivRing → 1 V ∈ Base V
15 eqid ⊢ 0 V = 0 V
16 15 12 drngunz ⊢ V ∈ DivRing → 1 V ≠ 0 V
17 9 16 syl ⊢ F ∈ DivRing → 1 V ≠ 0 V
18 11 15 lindssn ⊢ V ∈ LVec ∧ 1 V ∈ Base V ∧ 1 V ≠ 0 V → 1 V ∈ LIndS ⁡ V
19 3 14 17 18 syl3anc ⊢ F ∈ DivRing → 1 V ∈ LIndS ⁡ V
20 drngring ⊢ F ∈ DivRing → F ∈ Ring
21 1 fveq2i ⊢ LSpan ⁡ V = LSpan ⁡ ringLMod ⁡ F
22 rspval ⊢ RSpan ⁡ F = LSpan ⁡ ringLMod ⁡ F
23 21 22 eqtr4i ⊢ LSpan ⁡ V = RSpan ⁡ F
24 eqid ⊢ 1 F = 1 F
25 23 7 24 rsp1 ⊢ F ∈ Ring → LSpan ⁡ V ⁡ 1 F = Base F
26 20 25 syl ⊢ F ∈ DivRing → LSpan ⁡ V ⁡ 1 F = Base F
27 6 a1i ⊢ F ∈ DivRing → V = subringAlg ⁡ F ⁡ Base F
28 eqidd ⊢ F ∈ DivRing → 1 F = 1 F
29 ssidd ⊢ F ∈ DivRing → Base F ⊆ Base F
30 27 28 29 sra1r ⊢ F ∈ DivRing → 1 F = 1 V
31 30 sneqd ⊢ F ∈ DivRing → 1 F = 1 V
32 31 fveq2d ⊢ F ∈ DivRing → LSpan ⁡ V ⁡ 1 F = LSpan ⁡ V ⁡ 1 V
33 27 29 srabase ⊢ F ∈ DivRing → Base F = Base V
34 26 32 33 3eqtr3d ⊢ F ∈ DivRing → LSpan ⁡ V ⁡ 1 V = Base V
35 eqid ⊢ LBasis ⁡ V = LBasis ⁡ V
36 eqid ⊢ LSpan ⁡ V = LSpan ⁡ V
37 11 35 36 islbs4 ⊢ 1 V ∈ LBasis ⁡ V ↔ 1 V ∈ LIndS ⁡ V ∧ LSpan ⁡ V ⁡ 1 V = Base V
38 19 34 37 sylanbrc ⊢ F ∈ DivRing → 1 V ∈ LBasis ⁡ V
39 35 dimval ⊢ V ∈ LVec ∧ 1 V ∈ LBasis ⁡ V → dim ⁡ V = 1 V
40 3 38 39 syl2anc ⊢ F ∈ DivRing → dim ⁡ V = 1 V
41 fvex ⊢ 1 V ∈ V
42 hashsng ⊢ 1 V ∈ V → 1 V = 1
43 41 42 ax-mp ⊢ 1 V = 1
44 40 43 eqtrdi ⊢ F ∈ DivRing → dim ⁡ V = 1