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:AnormA1TAnormfnT

Proof

Step Hyp Ref Expression
1 nmfnsetre T:x|ynormy1x=Ty
2 ressxr *
3 1 2 sstrdi T:x|ynormy1x=Ty*
4 3 3ad2ant1 T:AnormA1x|ynormy1x=Ty*
5 fveq2 y=Anormy=normA
6 5 breq1d y=Anormy1normA1
7 2fveq3 y=ATy=TA
8 7 eqeq2d y=ATA=TyTA=TA
9 6 8 anbi12d y=Anormy1TA=TynormA1TA=TA
10 eqid TA=TA
11 10 biantru normA1normA1TA=TA
12 9 11 bitr4di y=Anormy1TA=TynormA1
13 12 rspcev AnormA1ynormy1TA=Ty
14 fvex TAV
15 eqeq1 x=TAx=TyTA=Ty
16 15 anbi2d x=TAnormy1x=Tynormy1TA=Ty
17 16 rexbidv x=TAynormy1x=Tyynormy1TA=Ty
18 14 17 elab TAx|ynormy1x=Tyynormy1TA=Ty
19 13 18 sylibr AnormA1TAx|ynormy1x=Ty
20 19 3adant1 T:AnormA1TAx|ynormy1x=Ty
21 supxrub x|ynormy1x=Ty*TAx|ynormy1x=TyTAsupx|ynormy1x=Ty*<
22 4 20 21 syl2anc T:AnormA1TAsupx|ynormy1x=Ty*<
23 nmfnval T:normfnT=supx|ynormy1x=Ty*<
24 23 3ad2ant1 T:AnormA1normfnT=supx|ynormy1x=Ty*<
25 22 24 breqtrrd T:AnormA1TAnormfnT