Metamath Proof Explorer

Theorem nmblore

Description: The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblore.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmblore.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmblore.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
nmblore.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
Assertion nmblore ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {N}\left({T}\right)\in ℝ$

Proof

Step Hyp Ref Expression
1 nmblore.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmblore.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmblore.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
4 nmblore.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
5 1 2 4 blof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}:{X}⟶{Y}$
6 1 2 3 nmogtmnf ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \mathrm{-\infty }<{N}\left({T}\right)$
7 5 6 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to \mathrm{-\infty }<{N}\left({T}\right)$
8 eqid ${⊢}{U}\mathrm{LnOp}{W}={U}\mathrm{LnOp}{W}$
9 3 8 4 isblo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {B}↔\left({T}\in \left({U}\mathrm{LnOp}{W}\right)\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)\right)$
10 9 simplbda ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {T}\in {B}\right)\to {N}\left({T}\right)<\mathrm{+\infty }$
11 10 3impa ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {N}\left({T}\right)<\mathrm{+\infty }$
12 1 2 3 nmoxr ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to {N}\left({T}\right)\in {ℝ}^{*}$
13 5 12 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {N}\left({T}\right)\in {ℝ}^{*}$
14 xrrebnd ${⊢}{N}\left({T}\right)\in {ℝ}^{*}\to \left({N}\left({T}\right)\in ℝ↔\left(\mathrm{-\infty }<{N}\left({T}\right)\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)\right)$
15 13 14 syl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to \left({N}\left({T}\right)\in ℝ↔\left(\mathrm{-\infty }<{N}\left({T}\right)\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)\right)$
16 7 11 15 mpbir2and ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {N}\left({T}\right)\in ℝ$