Metamath Proof Explorer

Theorem nvz0

Description: The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvz0.5 
|- Z = ( 0vec ` U )
nvz0.6 
|- N = ( normCV ` U )
Assertion nvz0 
|- ( U e. NrmCVec -> ( N ` Z ) = 0 )

Proof

Step Hyp Ref Expression
1 nvz0.5 
 |-  Z = ( 0vec ` U )
2 nvz0.6 
 |-  N = ( normCV ` U )
3 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
4 3 1 nvzcl 
 |-  ( U e. NrmCVec -> Z e. ( BaseSet ` U ) )
5 0re 
 |-  0 e. RR
6 0le0 
 |-  0 <_ 0
7 5 6 pm3.2i 
 |-  ( 0 e. RR /\ 0 <_ 0 )
8 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
9 3 8 2 nvsge0 
 |-  ( ( U e. NrmCVec /\ ( 0 e. RR /\ 0 <_ 0 ) /\ Z e. ( BaseSet ` U ) ) -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( 0 x. ( N ` Z ) ) )
10 7 9 mp3an2 
 |-  ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( 0 x. ( N ` Z ) ) )
11 4 10 mpdan 
 |-  ( U e. NrmCVec -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( 0 x. ( N ` Z ) ) )
12 3 8 1 nv0 
 |-  ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( 0 ( .sOLD ` U ) Z ) = Z )
13 4 12 mpdan 
 |-  ( U e. NrmCVec -> ( 0 ( .sOLD ` U ) Z ) = Z )
14 13 fveq2d 
 |-  ( U e. NrmCVec -> ( N ` ( 0 ( .sOLD ` U ) Z ) ) = ( N ` Z ) )
15 3 2 nvcl 
 |-  ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( N ` Z ) e. RR )
16 15 recnd 
 |-  ( ( U e. NrmCVec /\ Z e. ( BaseSet ` U ) ) -> ( N ` Z ) e. CC )
17 4 16 mpdan 
 |-  ( U e. NrmCVec -> ( N ` Z ) e. CC )
18 17 mul02d 
 |-  ( U e. NrmCVec -> ( 0 x. ( N ` Z ) ) = 0 )
19 11 14 18 3eqtr3d 
 |-  ( U e. NrmCVec -> ( N ` Z ) = 0 )