# Metamath Proof Explorer

## Theorem nmorepnf

Description: The norm of an operator is either real or plus infinity. (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 nmorepnf ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)\ne \mathrm{+\infty }\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 eqid ${⊢}{norm}_{CV}\left({W}\right)={norm}_{CV}\left({W}\right)$
5 2 4 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 ℝ$
6 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
7 eqid ${⊢}{norm}_{CV}\left({U}\right)={norm}_{CV}\left({U}\right)$
8 1 6 7 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\}$
9 8 ne0d ${⊢}{U}\in \mathrm{NrmCVec}\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\}\ne \varnothing$
10 supxrre2 ${⊢}\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 \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\}\ne \varnothing \right)\to \left(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)\in ℝ↔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)\ne \mathrm{+\infty }\right)$
11 5 9 10 syl2anr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\right)\to \left(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)\in ℝ↔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)\ne \mathrm{+\infty }\right)$
12 11 3impb ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left(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)\in ℝ↔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)\ne \mathrm{+\infty }\right)$
13 1 2 7 4 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)$
14 13 eleq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left({N}\left({T}\right)\in ℝ↔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)\in ℝ\right)$
15 13 neeq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left({N}\left({T}\right)\ne \mathrm{+\infty }↔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)\ne \mathrm{+\infty }\right)$
16 12 14 15 3bitr4d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)\ne \mathrm{+\infty }\right)$