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 )