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 = ( .sOLD ` U )
nvs.6 
|- N = ( normCV ` U )
Assertion nvm1 
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( -u 1 S A ) ) = ( N ` A ) )

Proof

Step Hyp Ref Expression
1 nvs.1 
 |-  X = ( BaseSet ` U )
2 nvs.4 
 |-  S = ( .sOLD ` U )
3 nvs.6 
 |-  N = ( normCV ` U )
4 neg1cn 
 |-  -u 1 e. CC
5 1 2 3 nvs 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( N ` ( -u 1 S A ) ) = ( ( abs ` -u 1 ) x. ( N ` A ) ) )
6 4 5 mp3an2 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( -u 1 S A ) ) = ( ( abs ` -u 1 ) x. ( N ` A ) ) )
7 ax-1cn 
 |-  1 e. CC
8 7 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
9 abs1 
 |-  ( abs ` 1 ) = 1
10 8 9 eqtri 
 |-  ( abs ` -u 1 ) = 1
11 10 oveq1i 
 |-  ( ( abs ` -u 1 ) x. ( N ` A ) ) = ( 1 x. ( N ` A ) )
12 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
13 12 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. CC )
14 13 mulid2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 x. ( N ` A ) ) = ( N ` A ) )
15 11 14 syl5eq 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( abs ` -u 1 ) x. ( N ` A ) ) = ( N ` A ) )
16 6 15 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( -u 1 S A ) ) = ( N ` A ) )