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 \in DivRing \to \dim (V) = 1$

Proof

Step	Hyp	Ref	Expression
1		rlmdim.1	$⊢ V = ringLMod (F)$
2		rlmlvec	$⊢ F \in DivRing \to ringLMod (F) \in LVec$
3	1 2	eqeltrid	$⊢ F \in DivRing \to V \in LVec$
4		ssid	$⊢ {Base}_{F} \subseteq {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 \in DivRing \land {Base}_{F} \subseteq {Base}_{F}) \to V \in DivRing$
9	4 8	mpan2	$⊢ F \in DivRing \to V \in DivRing$
10	9	drngringd	$⊢ F \in DivRing \to V \in Ring$
11		eqid	$⊢ {Base}_{V} = {Base}_{V}$
12		eqid	$⊢ 1_{V} = 1_{V}$
13	11 12	ringidcl	$⊢ V \in Ring \to 1_{V} \in {Base}_{V}$
14	10 13	syl	$⊢ F \in DivRing \to 1_{V} \in {Base}_{V}$
15		eqid	$⊢ 0_{V} = 0_{V}$
16	15 12	drngunz	$⊢ V \in DivRing \to 1_{V} \neq 0_{V}$
17	9 16	syl	$⊢ F \in DivRing \to 1_{V} \neq 0_{V}$
18	11 15	lindssn	$⊢ (V \in LVec \land 1_{V} \in {Base}_{V} \land 1_{V} \neq 0_{V}) \to \{1_{V}\} \in LIndS (V)$
19	3 14 17 18	syl3anc	$⊢ F \in DivRing \to \{1_{V}\} \in LIndS (V)$
20		drngring	$⊢ F \in DivRing \to F \in 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 \in Ring \to LSpan (V) (\{1_{F}\}) = {Base}_{F}$
26	20 25	syl	$⊢ F \in DivRing \to LSpan (V) (\{1_{F}\}) = {Base}_{F}$
27	6	a1i	$⊢ F \in DivRing \to V = subringAlg (F) ({Base}_{F})$
28		eqidd	$⊢ F \in DivRing \to 1_{F} = 1_{F}$
29		ssidd	$⊢ F \in DivRing \to {Base}_{F} \subseteq {Base}_{F}$
30	27 28 29	sra1r	$⊢ F \in DivRing \to 1_{F} = 1_{V}$
31	30	sneqd	$⊢ F \in DivRing \to \{1_{F}\} = \{1_{V}\}$
32	31	fveq2d	$⊢ F \in DivRing \to LSpan (V) (\{1_{F}\}) = LSpan (V) (\{1_{V}\})$
33	27 29	srabase	$⊢ F \in DivRing \to {Base}_{F} = {Base}_{V}$
34	26 32 33	3eqtr3d	$⊢ F \in DivRing \to 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}\} \in LBasis (V) \leftrightarrow (\{1_{V}\} \in LIndS (V) \land LSpan (V) (\{1_{V}\}) = {Base}_{V})$
38	19 34 37	sylanbrc	$⊢ F \in DivRing \to \{1_{V}\} \in LBasis (V)$
39	35	dimval	$⊢ (V \in LVec \land \{1_{V}\} \in LBasis (V)) \to \dim (V) = \|\{1_{V}\}\|$
40	3 38 39	syl2anc	$⊢ F \in DivRing \to \dim (V) = \|\{1_{V}\}\|$
41		fvex	$⊢ 1_{V} \in V$
42		hashsng	$⊢ 1_{V} \in V \to \|\{1_{V}\}\| = 1$
43	41 42	ax-mp	$⊢ \|\{1_{V}\}\| = 1$
44	40 43	eqtrdi	$⊢ F \in DivRing \to \dim (V) = 1$

Metamath Proof Explorer

Theorem rlmdim

Proof