Metamath Proof Explorer


Theorem nmoplb

Description: A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmoplb T : A norm A 1 norm T A norm op T

Proof

Step Hyp Ref Expression
1 nmopsetretHIL T : x | y norm y 1 x = norm T y
2 ressxr *
3 1 2 sstrdi T : x | y norm y 1 x = norm T y *
4 3 3ad2ant1 T : A norm A 1 x | y norm y 1 x = norm T y *
5 fveq2 y = A norm y = norm A
6 5 breq1d y = A norm y 1 norm A 1
7 2fveq3 y = A norm T y = norm T A
8 7 eqeq2d y = A norm T A = norm T y norm T A = norm T A
9 6 8 anbi12d y = A norm y 1 norm T A = norm T y norm A 1 norm T A = norm T A
10 eqid norm T A = norm T A
11 10 biantru norm A 1 norm A 1 norm T A = norm T A
12 9 11 bitr4di y = A norm y 1 norm T A = norm T y norm A 1
13 12 rspcev A norm A 1 y norm y 1 norm T A = norm T y
14 fvex norm T A V
15 eqeq1 x = norm T A x = norm T y norm T A = norm T y
16 15 anbi2d x = norm T A norm y 1 x = norm T y norm y 1 norm T A = norm T y
17 16 rexbidv x = norm T A y norm y 1 x = norm T y y norm y 1 norm T A = norm T y
18 14 17 elab norm T A x | y norm y 1 x = norm T y y norm y 1 norm T A = norm T y
19 13 18 sylibr A norm A 1 norm T A x | y norm y 1 x = norm T y
20 19 3adant1 T : A norm A 1 norm T A x | y norm y 1 x = norm T y
21 supxrub x | y norm y 1 x = norm T y * norm T A x | y norm y 1 x = norm T y norm T A sup x | y norm y 1 x = norm T y * <
22 4 20 21 syl2anc T : A norm A 1 norm T A sup x | y norm y 1 x = norm T y * <
23 nmopval T : norm op T = sup x | y norm y 1 x = norm T y * <
24 23 3ad2ant1 T : A norm A 1 norm op T = sup x | y norm y 1 x = norm T y * <
25 22 24 breqtrrd T : A norm A 1 norm T A norm op T