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 = ( BaseSet ` U )
nmblore.2 
|- Y = ( BaseSet ` W )
nmblore.3 
|- N = ( U normOpOLD W )
nmblore.5 
|- B = ( U BLnOp W )
Assertion nmblore 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( N ` T ) e. RR )

Proof

Step Hyp Ref Expression
1 nmblore.1 
 |-  X = ( BaseSet ` U )
2 nmblore.2 
 |-  Y = ( BaseSet ` W )
3 nmblore.3 
 |-  N = ( U normOpOLD W )
4 nmblore.5 
 |-  B = ( U BLnOp W )
5 1 2 4 blof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T : X --> Y )
6 1 2 3 nmogtmnf 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> -oo < ( N ` T ) )
7 5 6 syld3an3 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> -oo < ( N ` T ) )
8 eqid 
 |-  ( U LnOp W ) = ( U LnOp W )
9 3 8 4 isblo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> ( T e. ( U LnOp W ) /\ ( N ` T ) < +oo ) ) )
10 9 simplbda 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ T e. B ) -> ( N ` T ) < +oo )
11 10 3impa 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( N ` T ) < +oo )
12 1 2 3 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* )
13 5 12 syld3an3 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( N ` T ) e. RR* )
14 xrrebnd 
 |-  ( ( N ` T ) e. RR* -> ( ( N ` T ) e. RR <-> ( -oo < ( N ` T ) /\ ( N ` T ) < +oo ) ) )
15 13 14 syl 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( ( N ` T ) e. RR <-> ( -oo < ( N ` T ) /\ ( N ` T ) < +oo ) ) )
16 7 11 15 mpbir2and 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( N ` T ) e. RR )