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 )