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 e. Field -> ( dim ` V ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		rlmdim.1	\|- V = ( ringLMod ` F )
2		isfld	\|- ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
3	2	simplbi	\|- ( F e. Field -> F e. DivRing )
4		eqid	\|- ( Base ` F ) = ( Base ` F )
5	4	ressid	\|- ( F e. Field -> ( F \|`s ( Base ` F ) ) = F )
6	5 3	eqeltrd	\|- ( F e. Field -> ( F \|`s ( Base ` F ) ) e. DivRing )
7		drngring	\|- ( F e. DivRing -> F e. Ring )
8	4	subrgid	\|- ( F e. Ring -> ( Base ` F ) e. ( SubRing ` F ) )
9	3 7 8	3syl	\|- ( F e. Field -> ( Base ` F ) e. ( SubRing ` F ) )
10		rlmval	\|- ( ringLMod ` F ) = ( ( subringAlg ` F ) ` ( Base ` F ) )
11	1 10	eqtri	\|- V = ( ( subringAlg ` F ) ` ( Base ` F ) )
12		eqid	\|- ( F \|`s ( Base ` F ) ) = ( F \|`s ( Base ` F ) )
13	11 12	sralvec	\|- ( ( F e. DivRing /\ ( F \|`s ( Base ` F ) ) e. DivRing /\ ( Base ` F ) e. ( SubRing ` F ) ) -> V e. LVec )
14	3 6 9 13	syl3anc	\|- ( F e. Field -> V e. LVec )
15	3 7	syl	\|- ( F e. Field -> F e. Ring )
16		ssidd	\|- ( F e. Field -> ( Base ` F ) C_ ( Base ` F ) )
17	11 4	sraring	\|- ( ( F e. Ring /\ ( Base ` F ) C_ ( Base ` F ) ) -> V e. Ring )
18	15 16 17	syl2anc	\|- ( F e. Field -> V e. Ring )
19		eqid	\|- ( Base ` V ) = ( Base ` V )
20		eqid	\|- ( 1r ` V ) = ( 1r ` V )
21	19 20	ringidcl	\|- ( V e. Ring -> ( 1r ` V ) e. ( Base ` V ) )
22	18 21	syl	\|- ( F e. Field -> ( 1r ` V ) e. ( Base ` V ) )
23	11 4	sradrng	\|- ( ( F e. DivRing /\ ( Base ` F ) C_ ( Base ` F ) ) -> V e. DivRing )
24	3 16 23	syl2anc	\|- ( F e. Field -> V e. DivRing )
25		eqid	\|- ( 0g ` V ) = ( 0g ` V )
26	25 20	drngunz	\|- ( V e. DivRing -> ( 1r ` V ) =/= ( 0g ` V ) )
27	24 26	syl	\|- ( F e. Field -> ( 1r ` V ) =/= ( 0g ` V ) )
28	19 25	lindssn	\|- ( ( V e. LVec /\ ( 1r ` V ) e. ( Base ` V ) /\ ( 1r ` V ) =/= ( 0g ` V ) ) -> { ( 1r ` V ) } e. ( LIndS ` V ) )
29	14 22 27 28	syl3anc	\|- ( F e. Field -> { ( 1r ` V ) } e. ( 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 ) ` { ( 1r ` F ) } ) = ( ( LSpan ` V ) ` { ( 1r ` F ) } )
34		eqid	\|- ( RSpan ` F ) = ( RSpan ` F )
35		eqid	\|- ( 1r ` F ) = ( 1r ` F )
36	34 4 35	rsp1	\|- ( F e. Ring -> ( ( RSpan ` F ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
37	33 36	eqtr3id	\|- ( F e. Ring -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
38	3 7 37	3syl	\|- ( F e. Field -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( Base ` F ) )
39	11	a1i	\|- ( F e. Field -> V = ( ( subringAlg ` F ) ` ( Base ` F ) ) )
40		eqidd	\|- ( F e. Field -> ( 1r ` F ) = ( 1r ` F ) )
41	39 40 16	sra1r	\|- ( F e. Field -> ( 1r ` F ) = ( 1r ` V ) )
42	41	sneqd	\|- ( F e. Field -> { ( 1r ` F ) } = { ( 1r ` V ) } )
43	42	fveq2d	\|- ( F e. Field -> ( ( LSpan ` V ) ` { ( 1r ` F ) } ) = ( ( LSpan ` V ) ` { ( 1r ` V ) } ) )
44	39 16	srabase	\|- ( F e. Field -> ( Base ` F ) = ( Base ` V ) )
45	38 43 44	3eqtr3d	\|- ( F e. Field -> ( ( LSpan ` V ) ` { ( 1r ` V ) } ) = ( Base ` V ) )
46		eqid	\|- ( LBasis ` V ) = ( LBasis ` V )
47		eqid	\|- ( LSpan ` V ) = ( LSpan ` V )
48	19 46 47	islbs4	\|- ( { ( 1r ` V ) } e. ( LBasis ` V ) <-> ( { ( 1r ` V ) } e. ( LIndS ` V ) /\ ( ( LSpan ` V ) ` { ( 1r ` V ) } ) = ( Base ` V ) ) )
49	29 45 48	sylanbrc	\|- ( F e. Field -> { ( 1r ` V ) } e. ( LBasis ` V ) )
50	46	dimval	\|- ( ( V e. LVec /\ { ( 1r ` V ) } e. ( LBasis ` V ) ) -> ( dim ` V ) = ( # ` { ( 1r ` V ) } ) )
51	14 49 50	syl2anc	\|- ( F e. Field -> ( dim ` V ) = ( # ` { ( 1r ` V ) } ) )
52		fvex	\|- ( 1r ` V ) e. _V
53		hashsng	\|- ( ( 1r ` V ) e. _V -> ( # ` { ( 1r ` V ) } ) = 1 )
54	52 53	ax-mp	\|- ( # ` { ( 1r ` V ) } ) = 1
55	51 54	eqtrdi	\|- ( F e. Field -> ( dim ` V ) = 1 )

Metamath Proof Explorer

Theorem rgmoddimOLD

Proof