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=\mathrm{BaseSet}\left(U\right)$$
	nvmf.3	$$⊢M={-}_v\left(U\right)$$
Assertion	nvnnncan1	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(AMB\right)M\left(AMC\right)=CMB$$

Proof

Step	Hyp	Ref	Expression
1		nvmf.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvmf.3	$$⊢M={-}_v\left(U\right)$$
3		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
4	3	nvablo	$$⊢U\in \mathrm{NrmCVec}\to {+}_v\left(U\right)\in \mathrm{AbelOp}$$
5	1 3	bafval	$$⊢X=\mathrm{ran}{+}_v\left(U\right)$$
6	3 2	vsfval	$$⊢M={/}_g\left({+}_v\left(U\right)\right)$$
7	5 6	ablonnncan1	$$⊢\left({+}_v\left(U\right)\in \mathrm{AbelOp}\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(AMB\right)M\left(AMC\right)=CMB$$
8	4 7	sylan	$$⊢\left(U\in \mathrm{NrmCVec}\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(AMB\right)M\left(AMC\right)=CMB$$