Theorem clmadd

Description: The addition 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	clmadd	$$⊢W\in \mathrm{CMod}\to +={+}_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		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
5	3 4	ressplusg	$$⊢{\mathrm{Base}}_F\in \mathrm{V}\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
6	2 5	ax-mp	$$⊢+={+}_{\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 {+}_F={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
10	6 9	eqtr4id	$$⊢W\in \mathrm{CMod}\to +={+}_F$$