Theorem clmsub

Description: Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmsub.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	clmsub	$$⊢\left(W\in \mathrm{CMod}\wedge A\in K\wedge B\in K\right)\to A-B=A{-}_{F}B$$

Proof

Step	Hyp	Ref	Expression
1		clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		clmsub.k	$$⊢K={\mathrm{Base}}_F$$
3	1 2	clmsubrg	$$⊢W\in \mathrm{CMod}\to K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4		subrgsubg	$$⊢K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to K\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
5	3 4	syl	$$⊢W\in \mathrm{CMod}\to K\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
6		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
7		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
8		eqid	$$⊢{-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}={-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
9	6 7 8	subgsub	$$⊢\left(K\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge A\in K\wedge B\in K\right)\to A-B=A{-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}B$$
10	5 9	syl3an1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in K\wedge B\in K\right)\to A-B=A{-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}B$$
11	1 2	clmsca	$$⊢W\in \mathrm{CMod}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
12	11	fveq2d	$$⊢W\in \mathrm{CMod}\to {-}_F={-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
13	12	3ad2ant1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in K\wedge B\in K\right)\to {-}_F={-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}$$
14	13	oveqd	$$⊢\left(W\in \mathrm{CMod}\wedge A\in K\wedge B\in K\right)\to A{-}_{F}B=A{-}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\right)}B$$
15	10 14	eqtr4d	$$⊢\left(W\in \mathrm{CMod}\wedge A\in K\wedge B\in K\right)\to A-B=A{-}_{F}B$$