Theorem clmmul

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

	Ref	Expression
Hypothesis	clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	clmmul	$$⊢W\in \mathrm{CMod}\to \times ={\cdot }_F$$

Proof

Step	Hyp	Ref	Expression
1		clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
3	1 2	clmsca	$$⊢W\in \mathrm{CMod}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
4	3	fveq2d	$$⊢W\in \mathrm{CMod}\to {\cdot }_F={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
5		fvex	$$⊢{\mathrm{Base}}_F\in \mathrm{V}$$
6		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
7		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
8	6 7	ressmulr	$$⊢{\mathrm{Base}}_F\in \mathrm{V}\to \times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
9	5 8	ax-mp	$$⊢\times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
10	4 9	syl6reqr	$$⊢W\in \mathrm{CMod}\to \times ={\cdot }_F$$