Metamath Proof Explorer


Theorem nvnnncan1

Description: Cancellation law for vector subtraction. ( nnncan1 analog.) (Contributed by NM, 7-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvmf.1
|- X = ( BaseSet ` U )
nvmf.3
|- M = ( -v ` U )
Assertion nvnnncan1
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) )

Proof

Step Hyp Ref Expression
1 nvmf.1
 |-  X = ( BaseSet ` U )
2 nvmf.3
 |-  M = ( -v ` U )
3 eqid
 |-  ( +v ` U ) = ( +v ` U )
4 3 nvablo
 |-  ( U e. NrmCVec -> ( +v ` U ) e. AbelOp )
5 1 3 bafval
 |-  X = ran ( +v ` U )
6 3 2 vsfval
 |-  M = ( /g ` ( +v ` U ) )
7 5 6 ablonnncan1
 |-  ( ( ( +v ` U ) e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) )
8 4 7 sylan
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) )