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

Theorem nvz 22146
 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 2435 . . . . . 6
3 eqid 2435 . . . . . 6
4 nvz.5 . . . . . 6
5 nvz.6 . . . . . 6 CV
61, 2, 3, 4, 5nvi 22081 . . . . 5
76simp3d 971 . . . 4
8 simp1 957 . . . . 5
98ralimi 2773 . . . 4
10 fveq2 5719 . . . . . . 7
1110eqeq1d 2443 . . . . . 6
12 eqeq1 2441 . . . . . 6
1311, 12imbi12d 312 . . . . 5
1413rspccv 3041 . . . 4
157, 9, 143syl 19 . . 3
1615imp 419 . 2
17 fveq2 5719 . . . . 5
184, 5nvz0 22145 . . . . 5
1917, 18sylan9eqr 2489 . . . 4
2019ex 424 . . 3