Theorem lmodsubvs

Description: Subtraction of a scalar product in terms of addition. (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	lmodsubvs.v	$$⊢V={\mathrm{Base}}_W$$
	lmodsubvs.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lmodsubvs.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	lmodsubvs.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lmodsubvs.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lmodsubvs.k	$$⊢K={\mathrm{Base}}_F$$
	lmodsubvs.n	$$⊢N={inv}_g\left(F\right)$$
	lmodsubvs.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lmodsubvs.a	$$⊢\phi \to A\in K$$
	lmodsubvs.x	$$⊢\phi \to X\in V$$
	lmodsubvs.y	$$⊢\phi \to Y\in V$$
Assertion	lmodsubvs	$$⊢\phi \to X\underset{\dot{}}{-}\left(A\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{+}\left(N\left(A\right)\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmodsubvs.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodsubvs.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lmodsubvs.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		lmodsubvs.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		lmodsubvs.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
6		lmodsubvs.k	$$⊢K={\mathrm{Base}}_F$$
7		lmodsubvs.n	$$⊢N={inv}_g\left(F\right)$$
8		lmodsubvs.w	$$⊢\phi \to W\in \mathrm{LMod}$$
9		lmodsubvs.a	$$⊢\phi \to A\in K$$
10		lmodsubvs.x	$$⊢\phi \to X\in V$$
11		lmodsubvs.y	$$⊢\phi \to Y\in V$$
12	1 5 4 6	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in K\wedge Y\in V\right)\to A\underset{\dot{}}{·}Y\in V$$
13	8 9 11 12	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}Y\in V$$
14		eqid	$$⊢1_F=1_F$$
15	1 2 3 5 4 7 14	lmodvsubval2	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge A\underset{\dot{}}{·}Y\in V\right)\to X\underset{\dot{}}{-}\left(A\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{+}\left(N\left(1_F\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)\right)$$
16	8 10 13 15	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}\left(A\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{+}\left(N\left(1_F\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)\right)$$
17	5	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
18	8 17	syl	$$⊢\phi \to F\in \mathrm{Ring}$$
19		ringgrp	$$⊢F\in \mathrm{Ring}\to F\in \mathrm{Grp}$$
20	18 19	syl	$$⊢\phi \to F\in \mathrm{Grp}$$
21	6 14	ringidcl	$$⊢F\in \mathrm{Ring}\to 1_F\in K$$
22	18 21	syl	$$⊢\phi \to 1_F\in K$$
23	6 7	grpinvcl	$$⊢\left(F\in \mathrm{Grp}\wedge 1_F\in K\right)\to N\left(1_F\right)\in K$$
24	20 22 23	syl2anc	$$⊢\phi \to N\left(1_F\right)\in K$$
25		eqid	$$⊢{\cdot }_F={\cdot }_F$$
26	1 5 4 6 25	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(N\left(1_F\right)\in K\wedge A\in K\wedge Y\in V\right)\right)\to \left(N\left(1_F\right){\cdot }_{F}A\right)\underset{\dot{}}{·}Y=N\left(1_F\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)$$
27	8 24 9 11 26	syl13anc	$$⊢\phi \to \left(N\left(1_F\right){\cdot }_{F}A\right)\underset{\dot{}}{·}Y=N\left(1_F\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)$$
28	6 25 14 7 18 9	ringnegl	$$⊢\phi \to N\left(1_F\right){\cdot }_{F}A=N\left(A\right)$$
29	28	oveq1d	$$⊢\phi \to \left(N\left(1_F\right){\cdot }_{F}A\right)\underset{\dot{}}{·}Y=N\left(A\right)\underset{\dot{}}{·}Y$$
30	27 29	eqtr3d	$$⊢\phi \to N\left(1_F\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)=N\left(A\right)\underset{\dot{}}{·}Y$$
31	30	oveq2d	$$⊢\phi \to X\underset{\dot{}}{+}\left(N\left(1_F\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}Y\right)\right)=X\underset{\dot{}}{+}\left(N\left(A\right)\underset{\dot{}}{·}Y\right)$$
32	16 31	eqtrd	$$⊢\phi \to X\underset{\dot{}}{-}\left(A\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{+}\left(N\left(A\right)\underset{\dot{}}{·}Y\right)$$