Theorem clmcj

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