Metamath Proof Explorer


Theorem nmoleub2b

Description: The operator norm is the supremum of the value of a linear operator in the open unit ball. (Contributed by Mario Carneiro, 19-Oct-2015)

Ref Expression
Hypotheses nmoleub2.n
|- N = ( S normOp T )
nmoleub2.v
|- V = ( Base ` S )
nmoleub2.l
|- L = ( norm ` S )
nmoleub2.m
|- M = ( norm ` T )
nmoleub2.g
|- G = ( Scalar ` S )
nmoleub2.w
|- K = ( Base ` G )
nmoleub2.s
|- ( ph -> S e. ( NrmMod i^i CMod ) )
nmoleub2.t
|- ( ph -> T e. ( NrmMod i^i CMod ) )
nmoleub2.f
|- ( ph -> F e. ( S LMHom T ) )
nmoleub2.a
|- ( ph -> A e. RR* )
nmoleub2.r
|- ( ph -> R e. RR+ )
nmoleub2a.5
|- ( ph -> QQ C_ K )
Assertion nmoleub2b
|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )

Proof

Step Hyp Ref Expression
1 nmoleub2.n
 |-  N = ( S normOp T )
2 nmoleub2.v
 |-  V = ( Base ` S )
3 nmoleub2.l
 |-  L = ( norm ` S )
4 nmoleub2.m
 |-  M = ( norm ` T )
5 nmoleub2.g
 |-  G = ( Scalar ` S )
6 nmoleub2.w
 |-  K = ( Base ` G )
7 nmoleub2.s
 |-  ( ph -> S e. ( NrmMod i^i CMod ) )
8 nmoleub2.t
 |-  ( ph -> T e. ( NrmMod i^i CMod ) )
9 nmoleub2.f
 |-  ( ph -> F e. ( S LMHom T ) )
10 nmoleub2.a
 |-  ( ph -> A e. RR* )
11 nmoleub2.r
 |-  ( ph -> R e. RR+ )
12 nmoleub2a.5
 |-  ( ph -> QQ C_ K )
13 ltle
 |-  ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) < R -> ( L ` x ) <_ R ) )
14 idd
 |-  ( ( ( L ` x ) e. RR /\ R e. RR ) -> ( ( L ` x ) < R -> ( L ` x ) < R ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 nmoleub2lem2
 |-  ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ( L ` x ) < R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )