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 ) )