# Metamath Proof Explorer

## Theorem nmosetre

Description: The set in the supremum of the operator norm definition df-nmoo is a set of reals. (Contributed by NM, 13-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmosetre.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmosetre.4 ${⊢}{N}={norm}_{CV}\left({W}\right)$
Assertion nmosetre ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({z}\right)\le 1\wedge {x}={N}\left({T}\left({z}\right)\right)\right)\right\}\subseteq ℝ$

### Proof

Step Hyp Ref Expression
1 nmosetre.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
2 nmosetre.4 ${⊢}{N}={norm}_{CV}\left({W}\right)$
3 ffvelrn ${⊢}\left({T}:{X}⟶{Y}\wedge {z}\in {X}\right)\to {T}\left({z}\right)\in {Y}$
4 1 2 nvcl ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}\left({z}\right)\in {Y}\right)\to {N}\left({T}\left({z}\right)\right)\in ℝ$
5 3 4 sylan2 ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge \left({T}:{X}⟶{Y}\wedge {z}\in {X}\right)\right)\to {N}\left({T}\left({z}\right)\right)\in ℝ$
6 5 anassrs ${⊢}\left(\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\wedge {z}\in {X}\right)\to {N}\left({T}\left({z}\right)\right)\in ℝ$
7 eleq1 ${⊢}{x}={N}\left({T}\left({z}\right)\right)\to \left({x}\in ℝ↔{N}\left({T}\left({z}\right)\right)\in ℝ\right)$
8 6 7 syl5ibr ${⊢}{x}={N}\left({T}\left({z}\right)\right)\to \left(\left(\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\wedge {z}\in {X}\right)\to {x}\in ℝ\right)$
9 8 impcom ${⊢}\left(\left(\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\wedge {z}\in {X}\right)\wedge {x}={N}\left({T}\left({z}\right)\right)\right)\to {x}\in ℝ$
10 9 adantrl ${⊢}\left(\left(\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\wedge {z}\in {X}\right)\wedge \left({M}\left({z}\right)\le 1\wedge {x}={N}\left({T}\left({z}\right)\right)\right)\right)\to {x}\in ℝ$
11 10 rexlimdva2 ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left(\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({z}\right)\le 1\wedge {x}={N}\left({T}\left({z}\right)\right)\right)\to {x}\in ℝ\right)$
12 11 abssdv ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left\{{x}|\exists {z}\in {X}\phantom{\rule{.4em}{0ex}}\left({M}\left({z}\right)\le 1\wedge {x}={N}\left({T}\left({z}\right)\right)\right)\right\}\subseteq ℝ$