# Metamath Proof Explorer

## Theorem nmoxr

Description: The norm of an operator is an extended real. (Contributed by NM, 27-Nov-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 nmoxr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\right)\in {ℝ}^{*}$

### 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({U}\right)={norm}_{CV}\left({U}\right)$
5 eqid ${⊢}{norm}_{CV}\left({W}\right)={norm}_{CV}\left({W}\right)$
6 1 2 4 5 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)$
7 2 5 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 ℝ$
8 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
9 7 8 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 {ℝ}^{*}$
10 supxrcl ${⊢}\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 {ℝ}^{*}\to 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 {ℝ}^{*}$
11 9 10 syl ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to 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 {ℝ}^{*}$
12 11 3adant1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to 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 {ℝ}^{*}$
13 6 12 eqeltrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\right)\in {ℝ}^{*}$