rgmoddimOLD

Description: Obsolete version of rlmdim as of 21-Mar-2025. (Contributed by Thierry Arnoux, 5-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	rlmdim.1	$⊢ V = ringLMod (F)$
	Assertion	rgmoddimOLD	$⊢ F \in Field \to \dim (V) = 1$

Proof

Step	Hyp	Ref	Expression
1		rlmdim.1	$⊢ V = ringLMod (F)$
2		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
3	2	simplbi	$⊢ F \in Field \to F \in DivRing$
4		eqid	$⊢ {Base}_{F} = {Base}_{F}$
5	4	ressid	$⊢ F \in Field \to F ↾_{𝑠} {Base}_{F} = F$
6	5 3	eqeltrd	$⊢ F \in Field \to F ↾_{𝑠} {Base}_{F} \in DivRing$
7		drngring	$⊢ F \in DivRing \to F \in Ring$
8	4	subrgid	$⊢ F \in Ring \to {Base}_{F} \in SubRing (F)$
9	3 7 8	3syl	$⊢ F \in Field \to {Base}_{F} \in 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 \in DivRing \land F ↾_{𝑠} {Base}_{F} \in DivRing \land {Base}_{F} \in SubRing (F)) \to V \in LVec$
14	3 6 9 13	syl3anc	$⊢ F \in Field \to V \in LVec$
15	3 7	syl	$⊢ F \in Field \to F \in Ring$
16		ssidd	$⊢ F \in Field \to {Base}_{F} \subseteq {Base}_{F}$
17	11 4	sraring	$⊢ (F \in Ring \land {Base}_{F} \subseteq {Base}_{F}) \to V \in Ring$
18	15 16 17	syl2anc	$⊢ F \in Field \to V \in Ring$
19		eqid	$⊢ {Base}_{V} = {Base}_{V}$
20		eqid	$⊢ 1_{V} = 1_{V}$
21	19 20	ringidcl	$⊢ V \in Ring \to 1_{V} \in {Base}_{V}$
22	18 21	syl	$⊢ F \in Field \to 1_{V} \in {Base}_{V}$
23	11 4	sradrng	$⊢ (F \in DivRing \land {Base}_{F} \subseteq {Base}_{F}) \to V \in DivRing$
24	3 16 23	syl2anc	$⊢ F \in Field \to V \in DivRing$
25		eqid	$⊢ 0_{V} = 0_{V}$
26	25 20	drngunz	$⊢ V \in DivRing \to 1_{V} \neq 0_{V}$
27	24 26	syl	$⊢ F \in Field \to 1_{V} \neq 0_{V}$
28	19 25	lindssn	$⊢ (V \in LVec \land 1_{V} \in {Base}_{V} \land 1_{V} \neq 0_{V}) \to \{1_{V}\} \in LIndS (V)$
29	14 22 27 28	syl3anc	$⊢ F \in Field \to \{1_{V}\} \in 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 \in Ring \to RSpan (F) (\{1_{F}\}) = {Base}_{F}$
37	33 36	eqtr3id	$⊢ F \in Ring \to LSpan (V) (\{1_{F}\}) = {Base}_{F}$
38	3 7 37	3syl	$⊢ F \in Field \to LSpan (V) (\{1_{F}\}) = {Base}_{F}$
39	11	a1i	$⊢ F \in Field \to V = subringAlg (F) ({Base}_{F})$
40		eqidd	$⊢ F \in Field \to 1_{F} = 1_{F}$
41	39 40 16	sra1r	$⊢ F \in Field \to 1_{F} = 1_{V}$
42	41	sneqd	$⊢ F \in Field \to \{1_{F}\} = \{1_{V}\}$
43	42	fveq2d	$⊢ F \in Field \to LSpan (V) (\{1_{F}\}) = LSpan (V) (\{1_{V}\})$
44	39 16	srabase	$⊢ F \in Field \to {Base}_{F} = {Base}_{V}$
45	38 43 44	3eqtr3d	$⊢ F \in Field \to 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}\} \in LBasis (V) \leftrightarrow (\{1_{V}\} \in LIndS (V) \land LSpan (V) (\{1_{V}\}) = {Base}_{V})$
49	29 45 48	sylanbrc	$⊢ F \in Field \to \{1_{V}\} \in LBasis (V)$
50	46	dimval	$⊢ (V \in LVec \land \{1_{V}\} \in LBasis (V)) \to \dim (V) = \|\{1_{V}\}\|$
51	14 49 50	syl2anc	$⊢ F \in Field \to \dim (V) = \|\{1_{V}\}\|$
52		fvex	$⊢ 1_{V} \in V$
53		hashsng	$⊢ 1_{V} \in V \to \|\{1_{V}\}\| = 1$
54	52 53	ax-mp	$⊢ \|\{1_{V}\}\| = 1$
55	51 54	eqtrdi	$⊢ F \in Field \to \dim (V) = 1$

Metamath Proof Explorer

Theorem rgmoddimOLD

Proof