Metamath Proof Explorer


Theorem nvrcan

Description: Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvgcl.1
|- X = ( BaseSet ` U )
nvgcl.2
|- G = ( +v ` U )
Assertion nvrcan
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 nvgcl.1
 |-  X = ( BaseSet ` U )
2 nvgcl.2
 |-  G = ( +v ` U )
3 2 nvgrp
 |-  ( U e. NrmCVec -> G e. GrpOp )
4 1 2 bafval
 |-  X = ran G
5 4 grporcan
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )
6 3 5 sylan
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) = ( B G C ) <-> A = B ) )