Metamath Proof Explorer


Theorem lmodvsubval2

Description: Value of vector subtraction in terms of addition. ( hvsubval analog.) (Contributed by NM, 31-Mar-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvsubval2.v V=BaseW
lmodvsubval2.p +˙=+W
lmodvsubval2.m -˙=-W
lmodvsubval2.f F=ScalarW
lmodvsubval2.s ·˙=W
lmodvsubval2.n N=invgF
lmodvsubval2.u 1˙=1F
Assertion lmodvsubval2 WLModAVBVA-˙B=A+˙N1˙·˙B

Proof

Step Hyp Ref Expression
1 lmodvsubval2.v V=BaseW
2 lmodvsubval2.p +˙=+W
3 lmodvsubval2.m -˙=-W
4 lmodvsubval2.f F=ScalarW
5 lmodvsubval2.s ·˙=W
6 lmodvsubval2.n N=invgF
7 lmodvsubval2.u 1˙=1F
8 eqid invgW=invgW
9 1 2 8 3 grpsubval AVBVA-˙B=A+˙invgWB
10 9 3adant1 WLModAVBVA-˙B=A+˙invgWB
11 1 8 4 5 7 6 lmodvneg1 WLModBVN1˙·˙B=invgWB
12 11 3adant2 WLModAVBVN1˙·˙B=invgWB
13 12 oveq2d WLModAVBVA+˙N1˙·˙B=A+˙invgWB
14 10 13 eqtr4d WLModAVBVA-˙B=A+˙N1˙·˙B