# Metamath Proof Explorer

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 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
3 1 2 clmsca ${⊢}{W}\in \mathrm{CMod}\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}$
4 3 fveq2d ${⊢}{W}\in \mathrm{CMod}\to {+}_{{F}}={+}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)}$
5 fvex ${⊢}{\mathrm{Base}}_{{F}}\in \mathrm{V}$
6 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}$
7 cnfldadd ${⊢}+={+}_{{ℂ}_{\mathrm{fld}}}$
8 6 7 ressplusg ${⊢}{\mathrm{Base}}_{{F}}\in \mathrm{V}\to +={+}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)}$
9 5 8 ax-mp ${⊢}+={+}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)}$
10 4 9 syl6reqr ${⊢}{W}\in \mathrm{CMod}\to +={+}_{{F}}$