# Metamath Proof Explorer

## Theorem blo3i

Description: Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isblo3i.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
isblo3i.m ${⊢}{M}={norm}_{CV}\left({U}\right)$
isblo3i.n ${⊢}{N}={norm}_{CV}\left({W}\right)$
isblo3i.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
isblo3i.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
isblo3i.u ${⊢}{U}\in \mathrm{NrmCVec}$
isblo3i.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion blo3i ${⊢}\left({T}\in {L}\wedge {A}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {A}{M}\left({y}\right)\right)\to {T}\in {B}$

### Proof

Step Hyp Ref Expression
1 isblo3i.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 isblo3i.m ${⊢}{M}={norm}_{CV}\left({U}\right)$
3 isblo3i.n ${⊢}{N}={norm}_{CV}\left({W}\right)$
4 isblo3i.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
5 isblo3i.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
6 isblo3i.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 isblo3i.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 oveq1 ${⊢}{x}={A}\to {x}{M}\left({y}\right)={A}{M}\left({y}\right)$
9 8 breq2d ${⊢}{x}={A}\to \left({N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)↔{N}\left({T}\left({y}\right)\right)\le {A}{M}\left({y}\right)\right)$
10 9 ralbidv ${⊢}{x}={A}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {A}{M}\left({y}\right)\right)$
11 10 rspcev ${⊢}\left({A}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {A}{M}\left({y}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)$
12 1 2 3 4 5 6 7 isblo3i ${⊢}{T}\in {B}↔\left({T}\in {L}\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)$
13 12 biimpri ${⊢}\left({T}\in {L}\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to {T}\in {B}$
14 11 13 sylan2 ${⊢}\left({T}\in {L}\wedge \left({A}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {A}{M}\left({y}\right)\right)\right)\to {T}\in {B}$
15 14 3impb ${⊢}\left({T}\in {L}\wedge {A}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {A}{M}\left({y}\right)\right)\to {T}\in {B}$