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 φ S NrmMod CMod
nmoleub2.t φ T NrmMod CMod
nmoleub2.f φ F S LMHom T
nmoleub2.a φ A *
nmoleub2.r φ R +
nmoleub2a.5 φ K
Assertion nmoleub2b φ N F A x 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 φ S NrmMod CMod
8 nmoleub2.t φ T NrmMod CMod
9 nmoleub2.f φ F S LMHom T
10 nmoleub2.a φ A *
11 nmoleub2.r φ R +
12 nmoleub2a.5 φ K
13 ltle L x R L x < R L x R
14 idd L x R L x < R L x < R
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 nmoleub2lem2 φ N F A x V L x < R M F x R A