# 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}={0}_{\mathrm{vec}}\left({U}\right)$
nvz0.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
Assertion nvz0 ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left({Z}\right)=0$

### Proof

Step Hyp Ref Expression
1 nvz0.5 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
2 nvz0.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
3 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
4 3 1 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {Z}\in \mathrm{BaseSet}\left({U}\right)$
5 0re ${⊢}0\in ℝ$
6 0le0 ${⊢}0\le 0$
7 5 6 pm3.2i ${⊢}\left(0\in ℝ\wedge 0\le 0\right)$
8 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
9 3 8 2 nvsge0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(0\in ℝ\wedge 0\le 0\right)\wedge {Z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {N}\left(0{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Z}\right)=0\cdot {N}\left({Z}\right)$
10 7 9 mp3an2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {Z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {N}\left(0{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Z}\right)=0\cdot {N}\left({Z}\right)$
11 4 10 mpdan ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left(0{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Z}\right)=0\cdot {N}\left({Z}\right)$
12 3 8 1 nv0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {Z}\in \mathrm{BaseSet}\left({U}\right)\right)\to 0{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Z}={Z}$
13 4 12 mpdan ${⊢}{U}\in \mathrm{NrmCVec}\to 0{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Z}={Z}$
14 13 fveq2d ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left(0{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Z}\right)={N}\left({Z}\right)$
15 3 2 nvcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {Z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {N}\left({Z}\right)\in ℝ$
16 15 recnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {Z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {N}\left({Z}\right)\in ℂ$
17 4 16 mpdan ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left({Z}\right)\in ℂ$
18 17 mul02d ${⊢}{U}\in \mathrm{NrmCVec}\to 0\cdot {N}\left({Z}\right)=0$
19 11 14 18 3eqtr3d ${⊢}{U}\in \mathrm{NrmCVec}\to {N}\left({Z}\right)=0$