Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nvz Structured version   Unicode version

Theorem nvz 25999
 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.)
Hypotheses
Ref Expression
nvz.1
nvz.5
nvz.6 CV
Assertion
Ref Expression
nvz

Proof of Theorem nvz
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nvz.1 . . . . . 6
2 eqid 2404 . . . . . 6
3 eqid 2404 . . . . . 6
4 nvz.5 . . . . . 6
5 nvz.6 . . . . . 6 CV
61, 2, 3, 4, 5nvi 25934 . . . . 5
76simp3d 1013 . . . 4
8 simp1 999 . . . . 5
98ralimi 2799 . . . 4
10 fveq2 5851 . . . . . . 7
1110eqeq1d 2406 . . . . . 6
12 eqeq1 2408 . . . . . 6
1311, 12imbi12d 320 . . . . 5
1413rspccv 3159 . . . 4
157, 9, 143syl 18 . . 3
1615imp 429 . 2
17 fveq2 5851 . . . . 5
184, 5nvz0 25998 . . . . 5
1917, 18sylan9eqr 2467 . . . 4
2019ex 434 . . 3