# Metamath Proof Explorer

## Theorem nmooge0

Description: The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmoxr.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmoxr.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
Assertion nmooge0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to 0\le {N}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 nmoxr.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmoxr.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmoxr.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
4 0xr ${⊢}0\in {ℝ}^{*}$
5 4 a1i ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to 0\in {ℝ}^{*}$
6 simp2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {W}\in \mathrm{NrmCVec}$
7 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
8 1 7 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({U}\right)\in {X}$
9 ffvelrn ${⊢}\left({T}:{X}⟶{Y}\wedge {0}_{\mathrm{vec}}\left({U}\right)\in {X}\right)\to {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\in {Y}$
10 8 9 sylan2 ${⊢}\left({T}:{X}⟶{Y}\wedge {U}\in \mathrm{NrmCVec}\right)\to {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\in {Y}$
11 10 ancoms ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\in {Y}$
12 11 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\in {Y}$
13 eqid ${⊢}{norm}_{CV}\left({W}\right)={norm}_{CV}\left({W}\right)$
14 2 13 nvcl ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\in {Y}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\in ℝ$
15 6 12 14 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\in ℝ$
16 15 rexrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\in {ℝ}^{*}$
17 1 2 3 nmoxr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\right)\in {ℝ}^{*}$
18 2 13 nvge0 ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\in {Y}\right)\to 0\le {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)$
19 6 12 18 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to 0\le {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)$
20 2 13 nmosetre ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\}\subseteq ℝ$
21 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
22 20 21 sstrdi ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\}\subseteq {ℝ}^{*}$
23 eqid ${⊢}{norm}_{CV}\left({U}\right)={norm}_{CV}\left({U}\right)$
24 1 7 23 nmosetn0 ${⊢}{U}\in \mathrm{NrmCVec}\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\in \left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\}$
25 supxrub ${⊢}\left(\left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\in \left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\le sup\left(\left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
26 22 24 25 syl2an ${⊢}\left(\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\wedge {U}\in \mathrm{NrmCVec}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\le sup\left(\left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
27 26 3impa ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\wedge {U}\in \mathrm{NrmCVec}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\le sup\left(\left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
28 27 3comr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\le sup\left(\left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
29 1 2 23 13 3 nmooval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\right)=sup\left(\left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({norm}_{CV}\left({U}\right)\left({z}\right)\le 1\wedge {x}={norm}_{CV}\left({W}\right)\left({T}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
30 28 29 breqtrrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {norm}_{CV}\left({W}\right)\left({T}\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\le {N}\left({T}\right)$
31 5 16 17 19 30 xrletrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to 0\le {N}\left({T}\right)$