Metamath Proof Explorer


Theorem lmodvpncan

Description: Addition/subtraction cancellation law for vectors. ( hvpncan analog.) (Contributed by NM, 16-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmod4.v
|- V = ( Base ` W )
lmod4.p
|- .+ = ( +g ` W )
lmodvaddsub4.m
|- .- = ( -g ` W )
Assertion lmodvpncan
|- ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( ( A .+ B ) .- B ) = A )

Proof

Step Hyp Ref Expression
1 lmod4.v
 |-  V = ( Base ` W )
2 lmod4.p
 |-  .+ = ( +g ` W )
3 lmodvaddsub4.m
 |-  .- = ( -g ` W )
4 lmodgrp
 |-  ( W e. LMod -> W e. Grp )
5 1 2 3 grppncan
 |-  ( ( W e. Grp /\ A e. V /\ B e. V ) -> ( ( A .+ B ) .- B ) = A )
6 4 5 syl3an1
 |-  ( ( W e. LMod /\ A e. V /\ B e. V ) -> ( ( A .+ B ) .- B ) = A )