Theorem nvm1

Description: The norm of the negative of a vector. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvs.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nvs.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	nvs.6	$$⊢N={norm}_{CV}\left(U\right)$$
Assertion	nvm1	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(-1SA\right)=N\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nvs.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvs.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
3		nvs.6	$$⊢N={norm}_{CV}\left(U\right)$$
4		neg1cn	$$⊢-1\in ℂ$$
5	1 2 3	nvs	$$⊢\left(U\in \mathrm{NrmCVec}\wedge -1\in ℂ\wedge A\in X\right)\to N\left(-1SA\right)=\left|-1\right|N\left(A\right)$$
6	4 5	mp3an2	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(-1SA\right)=\left|-1\right|N\left(A\right)$$
7		ax-1cn	$$⊢1\in ℂ$$
8	7	absnegi	$$⊢\left|-1\right|=\left|1\right|$$
9		abs1	$$⊢\left|1\right|=1$$
10	8 9	eqtri	$$⊢\left|-1\right|=1$$
11	10	oveq1i	$$⊢\left|-1\right|N\left(A\right)=1N\left(A\right)$$
12	1 3	nvcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)\in ℝ$$
13	12	recnd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(A\right)\in ℂ$$
14	13	mullidd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to 1N\left(A\right)=N\left(A\right)$$
15	11 14	eqtrid	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to \left|-1\right|N\left(A\right)=N\left(A\right)$$
16	6 15	eqtrd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to N\left(-1SA\right)=N\left(A\right)$$