Theorem bj-rveccmod

Description: Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024)

	Ref	Expression
Assertion	bj-rveccmod	$$⊢V\in \mathrm{ℝVec}\to V\in \mathrm{CMod}$$

Proof

Step	Hyp	Ref	Expression
1		bj-rvecmod	$$⊢V\in \mathrm{ℝVec}\to V\in \mathrm{LMod}$$
2		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
3	2	a1i	$$⊢V\in \mathrm{ℝVec}\to {ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
4		resubdrg	$$⊢\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
5	4	simpli	$$⊢ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
6	5	a1i	$$⊢V\in \mathrm{ℝVec}\to ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
7		bj-rvecrr	$$⊢V\in \mathrm{ℝVec}\to \mathrm{Scalar}\left(V\right)={ℝ}_{\mathrm{fld}}$$
8	7	eqcomd	$$⊢V\in \mathrm{ℝVec}\to {ℝ}_{\mathrm{fld}}=\mathrm{Scalar}\left(V\right)$$
9		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
10	9	a1i	$$⊢V\in \mathrm{ℝVec}\to ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
11	8 10	bj-isclm	$$⊢V\in \mathrm{ℝVec}\to \left(V\in \mathrm{CMod}\leftrightarrow \left(V\in \mathrm{LMod}\wedge {ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ\wedge ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$
12	1 3 6 11	mpbir3and	$$⊢V\in \mathrm{ℝVec}\to V\in \mathrm{CMod}$$