Metamath Proof Explorer


Theorem nmopub

Description: An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopub T : A * norm op T A x norm x 1 norm T x A

Proof

Step Hyp Ref Expression
1 nmopval T : norm op T = sup y | x norm x 1 y = norm T x * <
2 1 adantr T : A * norm op T = sup y | x norm x 1 y = norm T x * <
3 2 breq1d T : A * norm op T A sup y | x norm x 1 y = norm T x * < A
4 nmopsetretALT T : y | x norm x 1 y = norm T x
5 ressxr *
6 4 5 sstrdi T : y | x norm x 1 y = norm T x *
7 supxrleub y | x norm x 1 y = norm T x * A * sup y | x norm x 1 y = norm T x * < A z y | x norm x 1 y = norm T x z A
8 6 7 sylan T : A * sup y | x norm x 1 y = norm T x * < A z y | x norm x 1 y = norm T x z A
9 ancom norm x 1 y = norm T x y = norm T x norm x 1
10 eqeq1 y = z y = norm T x z = norm T x
11 10 anbi1d y = z y = norm T x norm x 1 z = norm T x norm x 1
12 9 11 syl5bb y = z norm x 1 y = norm T x z = norm T x norm x 1
13 12 rexbidv y = z x norm x 1 y = norm T x x z = norm T x norm x 1
14 13 ralab z y | x norm x 1 y = norm T x z A z x z = norm T x norm x 1 z A
15 ralcom4 x z z = norm T x norm x 1 z A z x z = norm T x norm x 1 z A
16 impexp z = norm T x norm x 1 z A z = norm T x norm x 1 z A
17 16 albii z z = norm T x norm x 1 z A z z = norm T x norm x 1 z A
18 fvex norm T x V
19 breq1 z = norm T x z A norm T x A
20 19 imbi2d z = norm T x norm x 1 z A norm x 1 norm T x A
21 18 20 ceqsalv z z = norm T x norm x 1 z A norm x 1 norm T x A
22 17 21 bitri z z = norm T x norm x 1 z A norm x 1 norm T x A
23 22 ralbii x z z = norm T x norm x 1 z A x norm x 1 norm T x A
24 r19.23v x z = norm T x norm x 1 z A x z = norm T x norm x 1 z A
25 24 albii z x z = norm T x norm x 1 z A z x z = norm T x norm x 1 z A
26 15 23 25 3bitr3i x norm x 1 norm T x A z x z = norm T x norm x 1 z A
27 14 26 bitr4i z y | x norm x 1 y = norm T x z A x norm x 1 norm T x A
28 8 27 bitrdi T : A * sup y | x norm x 1 y = norm T x * < A x norm x 1 norm T x A
29 3 28 bitrd T : A * norm op T A x norm x 1 norm T x A