Metamath Proof Explorer


Theorem lmodsubdir

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

Ref Expression
Hypotheses lmodsubdir.v V=BaseW
lmodsubdir.t ·˙=W
lmodsubdir.f F=ScalarW
lmodsubdir.k K=BaseF
lmodsubdir.m -˙=-W
lmodsubdir.s S=-F
lmodsubdir.w φWLMod
lmodsubdir.a φAK
lmodsubdir.b φBK
lmodsubdir.x φXV
Assertion lmodsubdir φASB·˙X=A·˙X-˙B·˙X

Proof

Step Hyp Ref Expression
1 lmodsubdir.v V=BaseW
2 lmodsubdir.t ·˙=W
3 lmodsubdir.f F=ScalarW
4 lmodsubdir.k K=BaseF
5 lmodsubdir.m -˙=-W
6 lmodsubdir.s S=-F
7 lmodsubdir.w φWLMod
8 lmodsubdir.a φAK
9 lmodsubdir.b φBK
10 lmodsubdir.x φXV
11 3 lmodring WLModFRing
12 7 11 syl φFRing
13 ringgrp FRingFGrp
14 12 13 syl φFGrp
15 eqid invgF=invgF
16 4 15 grpinvcl FGrpBKinvgFBK
17 14 9 16 syl2anc φinvgFBK
18 eqid +W=+W
19 eqid +F=+F
20 1 18 3 2 4 19 lmodvsdir WLModAKinvgFBKXVA+FinvgFB·˙X=A·˙X+WinvgFB·˙X
21 7 8 17 10 20 syl13anc φA+FinvgFB·˙X=A·˙X+WinvgFB·˙X
22 eqid F=F
23 eqid 1F=1F
24 4 22 23 15 12 9 ringnegl φinvgF1FFB=invgFB
25 24 oveq1d φinvgF1FFB·˙X=invgFB·˙X
26 4 23 ringidcl FRing1FK
27 12 26 syl φ1FK
28 4 15 grpinvcl FGrp1FKinvgF1FK
29 14 27 28 syl2anc φinvgF1FK
30 1 3 2 4 22 lmodvsass WLModinvgF1FKBKXVinvgF1FFB·˙X=invgF1F·˙B·˙X
31 7 29 9 10 30 syl13anc φinvgF1FFB·˙X=invgF1F·˙B·˙X
32 25 31 eqtr3d φinvgFB·˙X=invgF1F·˙B·˙X
33 32 oveq2d φA·˙X+WinvgFB·˙X=A·˙X+WinvgF1F·˙B·˙X
34 21 33 eqtrd φA+FinvgFB·˙X=A·˙X+WinvgF1F·˙B·˙X
35 4 19 15 6 grpsubval AKBKASB=A+FinvgFB
36 8 9 35 syl2anc φASB=A+FinvgFB
37 36 oveq1d φASB·˙X=A+FinvgFB·˙X
38 1 3 2 4 lmodvscl WLModAKXVA·˙XV
39 7 8 10 38 syl3anc φA·˙XV
40 1 3 2 4 lmodvscl WLModBKXVB·˙XV
41 7 9 10 40 syl3anc φB·˙XV
42 1 18 5 3 2 15 23 lmodvsubval2 WLModA·˙XVB·˙XVA·˙X-˙B·˙X=A·˙X+WinvgF1F·˙B·˙X
43 7 39 41 42 syl3anc φA·˙X-˙B·˙X=A·˙X+WinvgF1F·˙B·˙X
44 34 37 43 3eqtr4d φASB·˙X=A·˙X-˙B·˙X