This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvpncan

Description: Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 
|- X = ( BaseSet ` U )
nvpncan2.2 
|- G = ( +v ` U )
nvpncan2.3 
|- M = ( -v ` U )
Assertion nvpncan 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M B ) = A )

Proof

Step Hyp Ref Expression
1 nvpncan2.1 
 |-  X = ( BaseSet ` U )
2 nvpncan2.2 
 |-  G = ( +v ` U )
3 nvpncan2.3 
 |-  M = ( -v ` U )
4 1 2 nvcom 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( B G A ) = ( A G B ) )
5 4 oveq1d 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( ( B G A ) M B ) = ( ( A G B ) M B ) )
6 1 2 3 nvpncan2 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( ( B G A ) M B ) = A )
7 5 6 eqtr3d 
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( ( A G B ) M B ) = A )
8 7 3com23 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A G B ) M B ) = A )