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 )