Metamath Proof Explorer

Theorem rgmoddim

Description: The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023)

Ref Expression
Hypothesis rgmoddim.1 ⊢ V = ringLMod ⁡ F
Assertion rgmoddim ⊢ F ∈ Field → dim ⁡ V = 1

Proof

Step Hyp Ref Expression
1 rgmoddim.1 ⊢ V = ringLMod ⁡ F
2 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
3 2 simplbi ⊢ F ∈ Field → F ∈ DivRing
4 eqid ⊢ Base F = Base F
5 4 ressid ⊢ F ∈ Field → F ↾ 𝑠 Base F = F
6 5 3 eqeltrd ⊢ F ∈ Field → F ↾ 𝑠 Base F ∈ DivRing
7 drngring ⊢ F ∈ DivRing → F ∈ Ring
8 4 subrgid ⊢ F ∈ Ring → Base F ∈ SubRing ⁡ F
9 3 7 8 3syl ⊢ F ∈ Field → Base F ∈ SubRing ⁡ F
10 rlmval ⊢ ringLMod ⁡ F = subringAlg ⁡ F ⁡ Base F
11 1 10 eqtri ⊢ V = subringAlg ⁡ F ⁡ Base F
12 eqid ⊢ F ↾ 𝑠 Base F = F ↾ 𝑠 Base F
13 11 12 sralvec ⊢ F ∈ DivRing ∧ F ↾ 𝑠 Base F ∈ DivRing ∧ Base F ∈ SubRing ⁡ F → V ∈ LVec
14 3 6 9 13 syl3anc ⊢ F ∈ Field → V ∈ LVec
15 3 7 syl ⊢ F ∈ Field → F ∈ Ring
16 ssidd ⊢ F ∈ Field → Base F ⊆ Base F
17 11 4 sraring ⊢ F ∈ Ring ∧ Base F ⊆ Base F → V ∈ Ring
18 15 16 17 syl2anc ⊢ F ∈ Field → V ∈ Ring
19 eqid ⊢ Base V = Base V
20 eqid ⊢ 1 V = 1 V
21 19 20 ringidcl ⊢ V ∈ Ring → 1 V ∈ Base V
22 18 21 syl ⊢ F ∈ Field → 1 V ∈ Base V
23 11 4 sradrng ⊢ F ∈ DivRing ∧ Base F ⊆ Base F → V ∈ DivRing
24 3 16 23 syl2anc ⊢ F ∈ Field → V ∈ DivRing
25 eqid ⊢ 0 V = 0 V
26 25 20 drngunz ⊢ V ∈ DivRing → 1 V ≠ 0 V
27 24 26 syl ⊢ F ∈ Field → 1 V ≠ 0 V
28 19 25 lindssn ⊢ V ∈ LVec ∧ 1 V ∈ Base V ∧ 1 V ≠ 0 V → 1 V ∈ LIndS ⁡ V
29 14 22 27 28 syl3anc ⊢ F ∈ Field → 1 V ∈ LIndS ⁡ V
30 rspval ⊢ RSpan ⁡ F = LSpan ⁡ ringLMod ⁡ F
31 1 fveq2i ⊢ LSpan ⁡ V = LSpan ⁡ ringLMod ⁡ F
32 30 31 eqtr4i ⊢ RSpan ⁡ F = LSpan ⁡ V
33 32 fveq1i ⊢ RSpan ⁡ F ⁡ 1 F = LSpan ⁡ V ⁡ 1 F
34 eqid ⊢ RSpan ⁡ F = RSpan ⁡ F
35 eqid ⊢ 1 F = 1 F
36 34 4 35 rsp1 ⊢ F ∈ Ring → RSpan ⁡ F ⁡ 1 F = Base F
37 33 36 eqtr3id ⊢ F ∈ Ring → LSpan ⁡ V ⁡ 1 F = Base F
38 3 7 37 3syl ⊢ F ∈ Field → LSpan ⁡ V ⁡ 1 F = Base F
39 11 a1i ⊢ F ∈ Field → V = subringAlg ⁡ F ⁡ Base F
40 eqidd ⊢ F ∈ Field → 1 F = 1 F
41 39 40 16 sra1r ⊢ F ∈ Field → 1 F = 1 V
42 41 sneqd ⊢ F ∈ Field → 1 F = 1 V
43 42 fveq2d ⊢ F ∈ Field → LSpan ⁡ V ⁡ 1 F = LSpan ⁡ V ⁡ 1 V
44 39 16 srabase ⊢ F ∈ Field → Base F = Base V
45 38 43 44 3eqtr3d ⊢ F ∈ Field → LSpan ⁡ V ⁡ 1 V = Base V
46 eqid ⊢ LBasis ⁡ V = LBasis ⁡ V
47 eqid ⊢ LSpan ⁡ V = LSpan ⁡ V
48 19 46 47 islbs4 ⊢ 1 V ∈ LBasis ⁡ V ↔ 1 V ∈ LIndS ⁡ V ∧ LSpan ⁡ V ⁡ 1 V = Base V
49 29 45 48 sylanbrc ⊢ F ∈ Field → 1 V ∈ LBasis ⁡ V
50 46 dimval ⊢ V ∈ LVec ∧ 1 V ∈ LBasis ⁡ V → dim ⁡ V = 1 V
51 14 49 50 syl2anc ⊢ F ∈ Field → dim ⁡ V = 1 V
52 fvex ⊢ 1 V ∈ V
53 hashsng ⊢ 1 V ∈ V → 1 V = 1
54 52 53 ax-mp ⊢ 1 V = 1
55 51 54 eqtrdi ⊢ F ∈ Field → dim ⁡ V = 1