Theorem clmmcl

Description: Closure of ring multiplication for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmsub.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	clmmcl	$$⊢\left(W\in \mathrm{CMod}\wedge X\in K\wedge Y\in K\right)\to XY\in K$$

Proof

Step	Hyp	Ref	Expression
1		clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		clmsub.k	$$⊢K={\mathrm{Base}}_F$$
3	1 2	clmsubrg	$$⊢W\in \mathrm{CMod}\to K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
5	4	subrgmcl	$$⊢\left(K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge X\in K\wedge Y\in K\right)\to XY\in K$$
6	3 5	syl3an1	$$⊢\left(W\in \mathrm{CMod}\wedge X\in K\wedge Y\in K\right)\to XY\in K$$