Metamath Proof Explorer

Theorem nvmtri

Description: Triangle inequality for the norm of a vector difference. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvmtri.1 
|- X = ( BaseSet ` U )
nvmtri.3 
|- M = ( -v ` U )
nvmtri.6 
|- N = ( normCV ` U )
Assertion nvmtri 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A M B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )

Proof

Step Hyp Ref Expression
1 nvmtri.1 
 |-  X = ( BaseSet ` U )
2 nvmtri.3 
 |-  M = ( -v ` U )
3 nvmtri.6 
 |-  N = ( normCV ` U )
4 neg1cn 
 |-  -u 1 e. CC
5 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
6 1 5 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) B ) e. X )
7 4 6 mp3an2 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) B ) e. X )
8 7 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 ( .sOLD ` U ) B ) e. X )
9 eqid 
 |-  ( +v ` U ) = ( +v ` U )
10 1 9 3 nvtri 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 ( .sOLD ` U ) B ) e. X ) -> ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) <_ ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) B ) ) ) )
11 8 10 syld3an3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) <_ ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) B ) ) ) )
12 1 9 5 2 nvmval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) )
13 12 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A M B ) ) = ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) B ) ) ) )
14 1 5 3 nvs 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( N ` ( -u 1 ( .sOLD ` U ) B ) ) = ( ( abs ` -u 1 ) x. ( N ` B ) ) )
15 4 14 mp3an2 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( N ` ( -u 1 ( .sOLD ` U ) B ) ) = ( ( abs ` -u 1 ) x. ( N ` B ) ) )
16 ax-1cn 
 |-  1 e. CC
17 16 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
18 abs1 
 |-  ( abs ` 1 ) = 1
19 17 18 eqtri 
 |-  ( abs ` -u 1 ) = 1
20 19 oveq1i 
 |-  ( ( abs ` -u 1 ) x. ( N ` B ) ) = ( 1 x. ( N ` B ) )
21 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( N ` B ) e. RR )
22 21 recnd 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( N ` B ) e. CC )
23 22 mulid2d 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( 1 x. ( N ` B ) ) = ( N ` B ) )
24 20 23 syl5eq 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( abs ` -u 1 ) x. ( N ` B ) ) = ( N ` B ) )
25 15 24 eqtr2d 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( N ` B ) = ( N ` ( -u 1 ( .sOLD ` U ) B ) ) )
26 25 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` B ) = ( N ` ( -u 1 ( .sOLD ` U ) B ) ) )
27 26 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` A ) + ( N ` B ) ) = ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) B ) ) ) )
28 11 13 27 3brtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A M B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )