Theorem clm0

Description: The zero 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	clm0	$$⊢W\in \mathrm{CMod}\to 0=0_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	clmsubrg	$$⊢W\in \mathrm{CMod}\to {\mathrm{Base}}_F\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
5		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
6	4 5	subrg0	$$⊢{\mathrm{Base}}_F\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
7	3 6	syl	$$⊢W\in \mathrm{CMod}\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
8	1 2	clmsca	$$⊢W\in \mathrm{CMod}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
9	8	fveq2d	$$⊢W\in \mathrm{CMod}\to 0_F=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
10	7 9	eqtr4d	$$⊢W\in \mathrm{CMod}\to 0=0_F$$