Theorem lmodsubdi

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr1 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014)

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

Proof

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