# Metamath Proof Explorer

## Theorem nmobndi

Description: Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion nmobndi ${⊢}{T}:{X}⟶{Y}\to \left({N}\left({T}\right)\in ℝ↔\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {r}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nmoubi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmoubi.y ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmoubi.l ${⊢}{L}={norm}_{CV}\left({U}\right)$
4 nmoubi.m ${⊢}{M}={norm}_{CV}\left({W}\right)$
5 nmoubi.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
6 nmoubi.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 nmoubi.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 leid ${⊢}{N}\left({T}\right)\in ℝ\to {N}\left({T}\right)\le {N}\left({T}\right)$
9 breq2 ${⊢}{r}={N}\left({T}\right)\to \left({N}\left({T}\right)\le {r}↔{N}\left({T}\right)\le {N}\left({T}\right)\right)$
10 9 rspcev ${⊢}\left({N}\left({T}\right)\in ℝ\wedge {N}\left({T}\right)\le {N}\left({T}\right)\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{N}\left({T}\right)\le {r}$
11 8 10 mpdan ${⊢}{N}\left({T}\right)\in ℝ\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{N}\left({T}\right)\le {r}$
12 1 2 5 nmoxr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\right)\in {ℝ}^{*}$
13 6 7 12 mp3an12 ${⊢}{T}:{X}⟶{Y}\to {N}\left({T}\right)\in {ℝ}^{*}$
14 13 adantr ${⊢}\left({T}:{X}⟶{Y}\wedge \left({r}\in ℝ\wedge {N}\left({T}\right)\le {r}\right)\right)\to {N}\left({T}\right)\in {ℝ}^{*}$
15 simprl ${⊢}\left({T}:{X}⟶{Y}\wedge \left({r}\in ℝ\wedge {N}\left({T}\right)\le {r}\right)\right)\to {r}\in ℝ$
16 1 2 5 nmogtmnf ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \mathrm{-\infty }<{N}\left({T}\right)$
17 6 7 16 mp3an12 ${⊢}{T}:{X}⟶{Y}\to \mathrm{-\infty }<{N}\left({T}\right)$
18 17 adantr ${⊢}\left({T}:{X}⟶{Y}\wedge \left({r}\in ℝ\wedge {N}\left({T}\right)\le {r}\right)\right)\to \mathrm{-\infty }<{N}\left({T}\right)$
19 simprr ${⊢}\left({T}:{X}⟶{Y}\wedge \left({r}\in ℝ\wedge {N}\left({T}\right)\le {r}\right)\right)\to {N}\left({T}\right)\le {r}$
20 xrre ${⊢}\left(\left({N}\left({T}\right)\in {ℝ}^{*}\wedge {r}\in ℝ\right)\wedge \left(\mathrm{-\infty }<{N}\left({T}\right)\wedge {N}\left({T}\right)\le {r}\right)\right)\to {N}\left({T}\right)\in ℝ$
21 14 15 18 19 20 syl22anc ${⊢}\left({T}:{X}⟶{Y}\wedge \left({r}\in ℝ\wedge {N}\left({T}\right)\le {r}\right)\right)\to {N}\left({T}\right)\in ℝ$
22 21 rexlimdvaa ${⊢}{T}:{X}⟶{Y}\to \left(\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{N}\left({T}\right)\le {r}\to {N}\left({T}\right)\in ℝ\right)$
23 11 22 impbid2 ${⊢}{T}:{X}⟶{Y}\to \left({N}\left({T}\right)\in ℝ↔\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{N}\left({T}\right)\le {r}\right)$
24 rexr ${⊢}{r}\in ℝ\to {r}\in {ℝ}^{*}$
25 1 2 3 4 5 6 7 nmoubi ${⊢}\left({T}:{X}⟶{Y}\wedge {r}\in {ℝ}^{*}\right)\to \left({N}\left({T}\right)\le {r}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {r}\right)\right)$
26 24 25 sylan2 ${⊢}\left({T}:{X}⟶{Y}\wedge {r}\in ℝ\right)\to \left({N}\left({T}\right)\le {r}↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {r}\right)\right)$
27 26 rexbidva ${⊢}{T}:{X}⟶{Y}\to \left(\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}{N}\left({T}\right)\le {r}↔\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {r}\right)\right)$
28 23 27 bitrd ${⊢}{T}:{X}⟶{Y}\to \left({N}\left({T}\right)\in ℝ↔\exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({L}\left({y}\right)\le 1\to {M}\left({T}\left({y}\right)\right)\le {r}\right)\right)$