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=\mathrm{BaseSet}\left(U\right)$$
	nvm.2	$$⊢G={+}_v\left(U\right)$$
	nvm.3	$$⊢M={-}_v\left(U\right)$$
	nvm.6	$$⊢N={/}_g\left(G\right)$$
Assertion	nvm	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to AMB=ANB$$

Proof

Step	Hyp	Ref	Expression
1		nvm.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvm.2	$$⊢G={+}_v\left(U\right)$$
3		nvm.3	$$⊢M={-}_v\left(U\right)$$
4		nvm.6	$$⊢N={/}_g\left(G\right)$$
5	2 3	vsfval	$$⊢M={/}_g\left(G\right)$$
6	5 4	eqtr4i	$$⊢M=N$$
7	6	oveqi	$$⊢AMB=ANB$$
8	7	a1i	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to AMB=ANB$$