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=\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)$$
Assertion	recvs	$$⊢R\in \mathrm{ℂVec}$$

Proof

Step	Hyp	Ref	Expression
1		recvs.r	$$⊢R=\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)$$
2		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
3		isfld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\leftrightarrow \left({ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
4	3	simprbi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℝ}_{\mathrm{fld}}\in \mathrm{CRing}$$
5	4	crngringd	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℝ}_{\mathrm{fld}}\in \mathrm{Ring}$$
6		rlmlmod	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LMod}$$
7	2 5 6	mp2b	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LMod}$$
8		rlmsca	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}\to {ℝ}_{\mathrm{fld}}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
9	2 8	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
10		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
11	9 10	eqtr3i	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
12		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
13	12	simpli	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
14		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\right)$$
15	14	isclmi	$$⊢\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\wedge ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{CMod}$$
16	7 11 13 15	mp3an	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{CMod}$$
17	12	simpri	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
18		rlmlvec	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\to \mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LVec}$$
19	17 18	ax-mp	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \mathrm{LVec}$$
20	16 19	elini	$$⊢\mathrm{ringLMod}\left({ℝ}_{\mathrm{fld}}\right)\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)$$
21		df-cvs	$$⊢\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$
22	20 1 21	3eltr4i	$$⊢R\in \mathrm{ℂVec}$$