Theorem clmvsubval

Description: Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 . (Contributed by NM, 31-Mar-2014) (Revised by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	clmvsubval.v	$$⊢V={\mathrm{Base}}_W$$
	clmvsubval.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	clmvsubval.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	clmvsubval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmvsubval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	clmvsubval	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{-}B=A\underset{\dot{}}{+}\left(-1\underset{\dot{}}{·}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		clmvsubval.v	$$⊢V={\mathrm{Base}}_W$$
2		clmvsubval.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		clmvsubval.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		clmvsubval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		clmvsubval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
7		eqid	$$⊢{inv}_g\left(F\right)={inv}_g\left(F\right)$$
8		eqid	$$⊢1_F=1_F$$
9	1 2 3 4 5 7 8	lmodvsubval2	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{-}B=A\underset{\dot{}}{+}\left({inv}_g\left(F\right)\left(1_F\right)\underset{\dot{}}{·}B\right)$$
10	6 9	syl3an1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{-}B=A\underset{\dot{}}{+}\left({inv}_g\left(F\right)\left(1_F\right)\underset{\dot{}}{·}B\right)$$
11	4	clm1	$$⊢W\in \mathrm{CMod}\to 1=1_F$$
12	11	eqcomd	$$⊢W\in \mathrm{CMod}\to 1_F=1$$
13	12	fveq2d	$$⊢W\in \mathrm{CMod}\to {inv}_g\left(F\right)\left(1_F\right)={inv}_g\left(F\right)\left(1\right)$$
14	4	clmring	$$⊢W\in \mathrm{CMod}\to F\in \mathrm{Ring}$$
15		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
16	15 8	ringidcl	$$⊢F\in \mathrm{Ring}\to 1_F\in {\mathrm{Base}}_F$$
17	14 16	syl	$$⊢W\in \mathrm{CMod}\to 1_F\in {\mathrm{Base}}_F$$
18	11 17	eqeltrd	$$⊢W\in \mathrm{CMod}\to 1\in {\mathrm{Base}}_F$$
19	4 15	clmneg	$$⊢\left(W\in \mathrm{CMod}\wedge 1\in {\mathrm{Base}}_F\right)\to -1={inv}_g\left(F\right)\left(1\right)$$
20	18 19	mpdan	$$⊢W\in \mathrm{CMod}\to -1={inv}_g\left(F\right)\left(1\right)$$
21	13 20	eqtr4d	$$⊢W\in \mathrm{CMod}\to {inv}_g\left(F\right)\left(1_F\right)=-1$$
22	21	3ad2ant1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\wedge B\in V\right)\to {inv}_g\left(F\right)\left(1_F\right)=-1$$
23	22	oveq1d	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\wedge B\in V\right)\to {inv}_g\left(F\right)\left(1_F\right)\underset{\dot{}}{·}B=-1\underset{\dot{}}{·}B$$
24	23	oveq2d	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{+}\left({inv}_g\left(F\right)\left(1_F\right)\underset{\dot{}}{·}B\right)=A\underset{\dot{}}{+}\left(-1\underset{\dot{}}{·}B\right)$$
25	10 24	eqtrd	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{-}B=A\underset{\dot{}}{+}\left(-1\underset{\dot{}}{·}B\right)$$