# Metamath Proof Explorer

## Theorem isblo3i

Description: The predicate "is a bounded linear operator." Definition 2.7-1 of Kreyszig p. 91. (Contributed by NM, 11-Dec-2007) (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 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)$

### 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 4 5 bloln ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}\in {L}$
9 6 7 8 mp3an12 ${⊢}{T}\in {B}\to {T}\in {L}$
10 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
11 eqid ${⊢}{U}{normOp}_{\mathrm{OLD}}{W}={U}{normOp}_{\mathrm{OLD}}{W}$
12 1 10 11 5 nmblore ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ$
13 6 7 12 mp3an12 ${⊢}{T}\in {B}\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ$
14 1 2 3 11 5 6 7 nmblolbi ${⊢}\left({T}\in {B}\wedge {y}\in {X}\right)\to {N}\left({T}\left({y}\right)\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right){M}\left({y}\right)$
15 14 ralrimiva ${⊢}{T}\in {B}\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right){M}\left({y}\right)$
16 oveq1 ${⊢}{x}=\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\to {x}{M}\left({y}\right)=\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right){M}\left({y}\right)$
17 16 breq2d ${⊢}{x}=\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\to \left({N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)↔{N}\left({T}\left({y}\right)\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right){M}\left({y}\right)\right)$
18 17 ralbidv ${⊢}{x}=\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\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 \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right){M}\left({y}\right)\right)$
19 18 rspcev ${⊢}\left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right){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)$
20 13 15 19 syl2anc ${⊢}{T}\in {B}\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)$
21 9 20 jca ${⊢}{T}\in {B}\to \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)$
22 simp1 ${⊢}\left({T}\in {L}\wedge {x}\in ℝ\wedge \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 {L}$
23 1 10 4 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:{X}⟶\mathrm{BaseSet}\left({W}\right)$
24 6 7 23 mp3an12 ${⊢}{T}\in {L}\to {T}:{X}⟶\mathrm{BaseSet}\left({W}\right)$
25 1 10 11 nmoxr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in {ℝ}^{*}$
26 6 7 25 mp3an12 ${⊢}{T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in {ℝ}^{*}$
27 26 3ad2ant1 ${⊢}\left({T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in {ℝ}^{*}$
28 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
29 28 abscld ${⊢}{x}\in ℝ\to \left|{x}\right|\in ℝ$
30 29 rexrd ${⊢}{x}\in ℝ\to \left|{x}\right|\in {ℝ}^{*}$
31 30 3ad2ant2 ${⊢}\left({T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \left|{x}\right|\in {ℝ}^{*}$
32 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
33 32 a1i ${⊢}\left({T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
34 1 10 2 3 11 6 7 nmoub3i ${⊢}\left({T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\le \left|{x}\right|$
35 ltpnf ${⊢}\left|{x}\right|\in ℝ\to \left|{x}\right|<\mathrm{+\infty }$
36 29 35 syl ${⊢}{x}\in ℝ\to \left|{x}\right|<\mathrm{+\infty }$
37 36 3ad2ant2 ${⊢}\left({T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \left|{x}\right|<\mathrm{+\infty }$
38 27 31 33 34 37 xrlelttrd ${⊢}\left({T}:{X}⟶\mathrm{BaseSet}\left({W}\right)\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)<\mathrm{+\infty }$
39 24 38 syl3an1 ${⊢}\left({T}\in {L}\wedge {x}\in ℝ\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({T}\left({y}\right)\right)\le {x}{M}\left({y}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)<\mathrm{+\infty }$
40 11 4 5 isblo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {B}↔\left({T}\in {L}\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)<\mathrm{+\infty }\right)\right)$
41 6 7 40 mp2an ${⊢}{T}\in {B}↔\left({T}\in {L}\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)<\mathrm{+\infty }\right)$
42 22 39 41 sylanbrc ${⊢}\left({T}\in {L}\wedge {x}\in ℝ\wedge \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}$
43 42 rexlimdv3a ${⊢}{T}\in {L}\to \left(\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)\to {T}\in {B}\right)$
44 43 imp ${⊢}\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}$
45 21 44 impbii ${⊢}{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)$