This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( ringLMod ‘ 𝐹 )
Assertion rlmdim ( 𝐹 ∈ DivRing → ( dim ‘ 𝑉 ) = 1 )

Proof

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