Metamath Proof Explorer

Theorem nmblolbi

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblolbi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmblolbi.4 ${⊢}{L}={norm}_{CV}\left({U}\right)$
nmblolbi.5 ${⊢}{M}={norm}_{CV}\left({W}\right)$
nmblolbi.6 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmblolbi.7 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
nmblolbi.u ${⊢}{U}\in \mathrm{NrmCVec}$
nmblolbi.w ${⊢}{W}\in \mathrm{NrmCVec}$
Assertion nmblolbi ${⊢}\left({T}\in {B}\wedge {A}\in {X}\right)\to {M}\left({T}\left({A}\right)\right)\le {N}\left({T}\right){L}\left({A}\right)$

Proof

Step Hyp Ref Expression
1 nmblolbi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmblolbi.4 ${⊢}{L}={norm}_{CV}\left({U}\right)$
3 nmblolbi.5 ${⊢}{M}={norm}_{CV}\left({W}\right)$
4 nmblolbi.6 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
5 nmblolbi.7 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
6 nmblolbi.u ${⊢}{U}\in \mathrm{NrmCVec}$
7 nmblolbi.w ${⊢}{W}\in \mathrm{NrmCVec}$
8 fveq1 ${⊢}{T}=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\to {T}\left({A}\right)=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\left({A}\right)$
9 8 fveq2d ${⊢}{T}=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\to {M}\left({T}\left({A}\right)\right)={M}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\left({A}\right)\right)$
10 fveq2 ${⊢}{T}=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\to {N}\left({T}\right)={N}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\right)$
11 10 oveq1d ${⊢}{T}=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\to {N}\left({T}\right){L}\left({A}\right)={N}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\right){L}\left({A}\right)$
12 9 11 breq12d ${⊢}{T}=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\to \left({M}\left({T}\left({A}\right)\right)\le {N}\left({T}\right){L}\left({A}\right)↔{M}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\left({A}\right)\right)\le {N}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\right){L}\left({A}\right)\right)$
13 12 imbi2d ${⊢}{T}=if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\to \left(\left({A}\in {X}\to {M}\left({T}\left({A}\right)\right)\le {N}\left({T}\right){L}\left({A}\right)\right)↔\left({A}\in {X}\to {M}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\left({A}\right)\right)\le {N}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\right){L}\left({A}\right)\right)\right)$
14 eqid ${⊢}{U}{0}_{\mathrm{op}}{W}={U}{0}_{\mathrm{op}}{W}$
15 14 5 0blo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {U}{0}_{\mathrm{op}}{W}\in {B}$
16 6 7 15 mp2an ${⊢}{U}{0}_{\mathrm{op}}{W}\in {B}$
17 16 elimel ${⊢}if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\in {B}$
18 1 2 3 4 5 6 7 17 nmblolbii ${⊢}{A}\in {X}\to {M}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\left({A}\right)\right)\le {N}\left(if\left({T}\in {B},{T},{U}{0}_{\mathrm{op}}{W}\right)\right){L}\left({A}\right)$
19 13 18 dedth ${⊢}{T}\in {B}\to \left({A}\in {X}\to {M}\left({T}\left({A}\right)\right)\le {N}\left({T}\right){L}\left({A}\right)\right)$
20 19 imp ${⊢}\left({T}\in {B}\wedge {A}\in {X}\right)\to {M}\left({T}\left({A}\right)\right)\le {N}\left({T}\right){L}\left({A}\right)$