Theorem nvm

Description: Vector subtraction in terms of group division operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nvm.1	|- X = ( BaseSet ` U )
2		nvm.2	|- G = ( +v ` U )
3		nvm.3	|- M = ( -v ` U )
4		nvm.6	|- N = ( /g ` G )
5	2 3	vsfval	|- M = ( /g ` G )
6	5 4	eqtr4i	|- M = N
7	6	oveqi	|- ( A M B ) = ( A N B )
8	7	a1i	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A N B ) )