This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvtri

Description: Triangle inequality for the norm of a normed complex vector space. (Contributed by NM, 11-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nvtri.1 
 |-  X = ( BaseSet ` U )
2 nvtri.2 
 |-  G = ( +v ` U )
3 nvtri.6 
 |-  N = ( normCV ` U )
4 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
5 4 smfval 
 |-  ( .sOLD ` U ) = ( 2nd ` ( 1st ` U ) )
6 5 eqcomi 
 |-  ( 2nd ` ( 1st ` U ) ) = ( .sOLD ` U )
7 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
8 1 2 6 7 3 nvi 
 |-  ( U e. NrmCVec -> ( <. G , ( 2nd ` ( 1st ` U ) ) >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y ( 2nd ` ( 1st ` U ) ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
9 8 simp3d 
 |-  ( U e. NrmCVec -> A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y ( 2nd ` ( 1st ` U ) ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
10 simp3 
 |-  ( ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y ( 2nd ` ( 1st ` U ) ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
11 10 ralimi 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( N ` ( y ( 2nd ` ( 1st ` U ) ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
12 9 11 syl 
 |-  ( U e. NrmCVec -> A. x e. X A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
13 fvoveq1 
 |-  ( x = A -> ( N ` ( x G y ) ) = ( N ` ( A G y ) ) )
14 fveq2 
 |-  ( x = A -> ( N ` x ) = ( N ` A ) )
15 14 oveq1d 
 |-  ( x = A -> ( ( N ` x ) + ( N ` y ) ) = ( ( N ` A ) + ( N ` y ) ) )
16 13 15 breq12d 
 |-  ( x = A -> ( ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) <-> ( N ` ( A G y ) ) <_ ( ( N ` A ) + ( N ` y ) ) ) )
17 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
18 17 fveq2d 
 |-  ( y = B -> ( N ` ( A G y ) ) = ( N ` ( A G B ) ) )
19 fveq2 
 |-  ( y = B -> ( N ` y ) = ( N ` B ) )
20 19 oveq2d 
 |-  ( y = B -> ( ( N ` A ) + ( N ` y ) ) = ( ( N ` A ) + ( N ` B ) ) )
21 18 20 breq12d 
 |-  ( y = B -> ( ( N ` ( A G y ) ) <_ ( ( N ` A ) + ( N ` y ) ) <-> ( N ` ( A G B ) ) <_ ( ( N ` A ) + ( N ` B ) ) ) )
22 16 21 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( N ` ( x G y ) ) <_ ( ( N ` x ) + ( N ` y ) ) -> ( N ` ( A G B ) ) <_ ( ( N ` A ) + ( N ` B ) ) ) )
23 12 22 syl5 
 |-  ( ( A e. X /\ B e. X ) -> ( U e. NrmCVec -> ( N ` ( A G B ) ) <_ ( ( N ` A ) + ( N ` B ) ) ) )
24 23 3impia 
 |-  ( ( A e. X /\ B e. X /\ U e. NrmCVec ) -> ( N ` ( A G B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )
25 24 3comr 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G B ) ) <_ ( ( N ` A ) + ( N ` B ) ) )