Metamath Proof Explorer


Theorem nmfnlb

Description: A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnlb T : A norm A 1 T A norm fn T

Proof

Step Hyp Ref Expression
1 nmfnsetre T : x | y norm y 1 x = T y
2 ressxr *
3 1 2 sstrdi T : x | y norm y 1 x = T y *
4 3 3ad2ant1 T : A norm A 1 x | y norm y 1 x = 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 T y = T A
8 7 eqeq2d y = A T A = T y T A = T A
9 6 8 anbi12d y = A norm y 1 T A = T y norm A 1 T A = T A
10 eqid T A = T A
11 10 biantru norm A 1 norm A 1 T A = T A
12 9 11 bitr4di y = A norm y 1 T A = T y norm A 1
13 12 rspcev A norm A 1 y norm y 1 T A = T y
14 fvex T A V
15 eqeq1 x = T A x = T y T A = T y
16 15 anbi2d x = T A norm y 1 x = T y norm y 1 T A = T y
17 16 rexbidv x = T A y norm y 1 x = T y y norm y 1 T A = T y
18 14 17 elab T A x | y norm y 1 x = T y y norm y 1 T A = T y
19 13 18 sylibr A norm A 1 T A x | y norm y 1 x = T y
20 19 3adant1 T : A norm A 1 T A x | y norm y 1 x = T y
21 supxrub x | y norm y 1 x = T y * T A x | y norm y 1 x = T y T A sup x | y norm y 1 x = T y * <
22 4 20 21 syl2anc T : A norm A 1 T A sup x | y norm y 1 x = T y * <
23 nmfnval T : norm fn T = sup x | y norm y 1 x = T y * <
24 23 3ad2ant1 T : A norm A 1 norm fn T = sup x | y norm y 1 x = T y * <
25 22 24 breqtrrd T : A norm A 1 T A norm fn T