Theorem qcvs

Description: The field of rational 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)

	Ref	Expression
Hypothesis	qcvs.q	$$⊢Q=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
Assertion	qcvs	$$⊢Q\in \mathrm{ℂVec}$$

Proof

Step	Hyp	Ref	Expression
1		qcvs.q	$$⊢Q=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
2		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
3		drngring	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{Ring}$$
4	3	adantl	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{Ring}$$
5	2 4	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{Ring}$$
6		rlmlmod	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{LMod}$$
7	5 6	ax-mp	$$⊢\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{LMod}$$
8	2	simpri	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}$$
9		rlmsca	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)$$
10	9	eqcomd	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
11	8 10	ax-mp	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
12	2	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
13		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)$$
14	13	isclmi	$$⊢\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\wedge \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{CMod}$$
15	7 11 12 14	mp3an	$$⊢\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{CMod}$$
16		rlmlvec	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\to \mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{LVec}$$
17	8 16	ax-mp	$$⊢\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \mathrm{LVec}$$
18	15 17	elini	$$⊢\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)$$
19		df-cvs	$$⊢\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$
20	18 1 19	3eltr4i	$$⊢Q\in \mathrm{ℂVec}$$