Metamath Proof Explorer

Theorem nmoub2i

Description: An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007) (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 nmoub2i ${⊢}\left({T}:{X}⟶{Y}\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le {A}$

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 1 2 3 4 5 6 7 nmoub3i ${⊢}\left({T}:{X}⟶{Y}\wedge {A}\in ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le \left|{A}\right|$
9 8 3adant2r ${⊢}\left({T}:{X}⟶{Y}\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le \left|{A}\right|$
10 absid ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to \left|{A}\right|={A}$
11 10 3ad2ant2 ${⊢}\left({T}:{X}⟶{Y}\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to \left|{A}\right|={A}$
12 9 11 breqtrd ${⊢}\left({T}:{X}⟶{Y}\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{M}\left({T}\left({x}\right)\right)\le {A}{L}\left({x}\right)\right)\to {N}\left({T}\right)\le {A}$