Theorem clm1

Description: The identity 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	clm1	$$⊢W\in \mathrm{CMod}\to 1=1_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		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
6	4 5	subrg1	$$⊢{\mathrm{Base}}_F\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to 1=1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
7	3 6	syl	$$⊢W\in \mathrm{CMod}\to 1=1_{\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 1_F=1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)}$$
10	7 9	eqtr4d	$$⊢W\in \mathrm{CMod}\to 1=1_F$$