Theorem lmodsubdir

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr2 analog.) (Contributed by NM, 2-Jul-2014)

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

Proof

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