Metamath Proof Explorer


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 = BaseSet U
nvs.4 S = 𝑠OLD U
nvs.6 N = norm CV U
Assertion nvm1 U NrmCVec A X N -1 S A = N A

Proof

Step Hyp Ref Expression
1 nvs.1 X = BaseSet U
2 nvs.4 S = 𝑠OLD U
3 nvs.6 N = norm CV U
4 neg1cn 1
5 1 2 3 nvs U NrmCVec 1 A X N -1 S A = 1 N A
6 4 5 mp3an2 U NrmCVec A X N -1 S A = 1 N A
7 ax-1cn 1
8 7 absnegi 1 = 1
9 abs1 1 = 1
10 8 9 eqtri 1 = 1
11 10 oveq1i 1 N A = 1 N A
12 1 3 nvcl U NrmCVec A X N A
13 12 recnd U NrmCVec A X N A
14 13 mulid2d U NrmCVec A X 1 N A = N A
15 11 14 syl5eq U NrmCVec A X 1 N A = N A
16 6 15 eqtrd U NrmCVec A X N -1 S A = N A