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		fvex	$$⊢{\mathrm{Base}}_F\in \mathrm{V}$$
3		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
4		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
5	3 4	ressmulr	$$⊢{\mathrm{Base}}_F\in \mathrm{V}\to \times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
6	2 5	ax-mp	$$⊢\times ={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
7		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
8	1 7	clmsca	$$⊢W\in \mathrm{CMod}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
9	8	fveq2d	$$⊢W\in \mathrm{CMod}\to {\cdot }_F={\cdot }_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
10	6 9	eqtr4id	$$⊢W\in \mathrm{CMod}\to \times ={\cdot }_F$$