Metamath Proof Explorer

Theorem nvz

Description: The norm of a vector is zero iff the vector is zero. First part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nvz.1 
 |-  X = ( BaseSet ` U )
2 nvz.5 
 |-  Z = ( 0vec ` U )
3 nvz.6 
 |-  N = ( normCV ` U )
4 eqid 
 |-  ( +v ` U ) = ( +v ` U )
5 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
6 1 4 5 2 3 nvi 
 |-  ( U e. NrmCVec -> ( <. ( +v ` U ) , ( .sOLD ` U ) >. e. CVecOLD /\ N : X --> RR /\ A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y ( .sOLD ` U ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
7 6 simp3d 
 |-  ( U e. NrmCVec -> A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y ( .sOLD ` U ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) )
8 simp1 
 |-  ( ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y ( .sOLD ` U ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( ( N ` x ) = 0 -> x = Z ) )
9 8 ralimi 
 |-  ( A. x e. X ( ( ( N ` x ) = 0 -> x = Z ) /\ A. y e. CC ( N ` ( y ( .sOLD ` U ) x ) ) = ( ( abs ` y ) x. ( N ` x ) ) /\ A. y e. X ( N ` ( x ( +v ` U ) y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> A. x e. X ( ( N ` x ) = 0 -> x = Z ) )
10 fveqeq2 
 |-  ( x = A -> ( ( N ` x ) = 0 <-> ( N ` A ) = 0 ) )
11 eqeq1 
 |-  ( x = A -> ( x = Z <-> A = Z ) )
12 10 11 imbi12d 
 |-  ( x = A -> ( ( ( N ` x ) = 0 -> x = Z ) <-> ( ( N ` A ) = 0 -> A = Z ) ) )
13 12 rspccv 
 |-  ( A. x e. X ( ( N ` x ) = 0 -> x = Z ) -> ( A e. X -> ( ( N ` A ) = 0 -> A = Z ) ) )
14 7 9 13 3syl 
 |-  ( U e. NrmCVec -> ( A e. X -> ( ( N ` A ) = 0 -> A = Z ) ) )
15 14 imp 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) = 0 -> A = Z ) )
16 fveq2 
 |-  ( A = Z -> ( N ` A ) = ( N ` Z ) )
17 2 3 nvz0 
 |-  ( U e. NrmCVec -> ( N ` Z ) = 0 )
18 16 17 sylan9eqr 
 |-  ( ( U e. NrmCVec /\ A = Z ) -> ( N ` A ) = 0 )
19 18 ex 
 |-  ( U e. NrmCVec -> ( A = Z -> ( N ` A ) = 0 ) )
20 19 adantr 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A = Z -> ( N ` A ) = 0 ) )
21 15 20 impbid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = Z ) )