Metamath Proof Explorer

Theorem nvge0

Description: The norm of a normed complex vector space is nonnegative. Second part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 28-Nov-2006) (Proof shortened by AV, 10-Jul-2022) (New usage is discouraged.)

Ref Expression
Hypotheses nvge0.1 
|- X = ( BaseSet ` U )
nvge0.6 
|- N = ( normCV ` U )
Assertion nvge0 
|- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )

Proof

Step Hyp Ref Expression
1 nvge0.1 
 |-  X = ( BaseSet ` U )
2 nvge0.6 
 |-  N = ( normCV ` U )
3 2rp 
 |-  2 e. RR+
4 3 a1i 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 2 e. RR+ )
5 1 2 nvcl 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
6 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
7 6 2 nvz0 
 |-  ( U e. NrmCVec -> ( N ` ( 0vec ` U ) ) = 0 )
8 7 adantr 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( 0vec ` U ) ) = 0 )
9 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
10 9 oveq1i 
 |-  ( ( 1 + -u 1 ) ( .sOLD ` U ) A ) = ( 0 ( .sOLD ` U ) A )
11 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
12 1 11 6 nv0 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 0 ( .sOLD ` U ) A ) = ( 0vec ` U ) )
13 10 12 eqtr2id 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 0vec ` U ) = ( ( 1 + -u 1 ) ( .sOLD ` U ) A ) )
14 neg1cn 
 |-  -u 1 e. CC
15 ax-1cn 
 |-  1 e. CC
16 eqid 
 |-  ( +v ` U ) = ( +v ` U )
17 1 16 11 nvdir 
 |-  ( ( U e. NrmCVec /\ ( 1 e. CC /\ -u 1 e. CC /\ A e. X ) ) -> ( ( 1 + -u 1 ) ( .sOLD ` U ) A ) = ( ( 1 ( .sOLD ` U ) A ) ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) )
18 15 17 mp3anr1 
 |-  ( ( U e. NrmCVec /\ ( -u 1 e. CC /\ A e. X ) ) -> ( ( 1 + -u 1 ) ( .sOLD ` U ) A ) = ( ( 1 ( .sOLD ` U ) A ) ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) )
19 14 18 mpanr1 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( 1 + -u 1 ) ( .sOLD ` U ) A ) = ( ( 1 ( .sOLD ` U ) A ) ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) )
20 1 11 nvsid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 ( .sOLD ` U ) A ) = A )
21 20 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( 1 ( .sOLD ` U ) A ) ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) )
22 13 19 21 3eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 0vec ` U ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) )
23 22 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( 0vec ` U ) ) = ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) )
24 8 23 eqtr3d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 0 = ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) )
25 1 11 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 ( .sOLD ` U ) A ) e. X )
26 14 25 mp3an2 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 ( .sOLD ` U ) A ) e. X )
27 1 16 2 nvtri 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 ( .sOLD ` U ) A ) e. X ) -> ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) <_ ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) A ) ) ) )
28 26 27 mpd3an3 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) A ) ) ) <_ ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) A ) ) ) )
29 24 28 eqbrtrd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) A ) ) ) )
30 1 11 2 nvm1 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( -u 1 ( .sOLD ` U ) A ) ) = ( N ` A ) )
31 30 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) A ) ) ) = ( ( N ` A ) + ( N ` A ) ) )
32 5 recnd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. CC )
33 32 2timesd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 2 x. ( N ` A ) ) = ( ( N ` A ) + ( N ` A ) ) )
34 31 33 eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) + ( N ` ( -u 1 ( .sOLD ` U ) A ) ) ) = ( 2 x. ( N ` A ) ) )
35 29 34 breqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( 2 x. ( N ` A ) ) )
36 4 5 35 prodge0rd 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )