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

Proof

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