Theorem recvs

Description: The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by AV, 22-Oct-2021) (Proof shortened by SN, 23-Nov-2024)

	Ref	Expression
Hypothesis	recvs.r	|- R = ( ringLMod ` RRfld )
Assertion	recvs	|- R e. CVec

Proof

Step	Hyp	Ref	Expression
1		recvs.r	|- R = ( ringLMod ` RRfld )
2		refld	|- RRfld e. Field
3		isfld	|- ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
4	3	simprbi	|- ( RRfld e. Field -> RRfld e. CRing )
5	4	crngringd	|- ( RRfld e. Field -> RRfld e. Ring )
6		rlmlmod	|- ( RRfld e. Ring -> ( ringLMod ` RRfld ) e. LMod )
7	2 5 6	mp2b	|- ( ringLMod ` RRfld ) e. LMod
8		rlmsca	|- ( RRfld e. Field -> RRfld = ( Scalar ` ( ringLMod ` RRfld ) ) )
9	2 8	ax-mp	|- RRfld = ( Scalar ` ( ringLMod ` RRfld ) )
10		df-refld	|- RRfld = ( CCfld |`s RR )
11	9 10	eqtr3i	|- ( Scalar ` ( ringLMod ` RRfld ) ) = ( CCfld |`s RR )
12		resubdrg	|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
13	12	simpli	|- RR e. ( SubRing ` CCfld )
14		eqid	|- ( Scalar ` ( ringLMod ` RRfld ) ) = ( Scalar ` ( ringLMod ` RRfld ) )
15	14	isclmi	|- ( ( ( ringLMod ` RRfld ) e. LMod /\ ( Scalar ` ( ringLMod ` RRfld ) ) = ( CCfld |`s RR ) /\ RR e. ( SubRing ` CCfld ) ) -> ( ringLMod ` RRfld ) e. CMod )
16	7 11 13 15	mp3an	|- ( ringLMod ` RRfld ) e. CMod
17	12	simpri	|- RRfld e. DivRing
18		rlmlvec	|- ( RRfld e. DivRing -> ( ringLMod ` RRfld ) e. LVec )
19	17 18	ax-mp	|- ( ringLMod ` RRfld ) e. LVec
20	16 19	elini	|- ( ringLMod ` RRfld ) e. ( CMod i^i LVec )
21		df-cvs	|- CVec = ( CMod i^i LVec )
22	20 1 21	3eltr4i	|- R e. CVec