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 ) ) ) |
| 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 ) ) ) |