Metamath Proof Explorer


Theorem nmcfnlb

Description: A lower bound of the norm of a continuous linear Hilbert space functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmcfnlb TLinFnTContFnATAnormfnTnormA

Proof

Step Hyp Ref Expression
1 elin TLinFnContFnTLinFnTContFn
2 fveq1 T=ifTLinFnContFnT×0TA=ifTLinFnContFnT×0A
3 2 fveq2d T=ifTLinFnContFnT×0TA=ifTLinFnContFnT×0A
4 fveq2 T=ifTLinFnContFnT×0normfnT=normfnifTLinFnContFnT×0
5 4 oveq1d T=ifTLinFnContFnT×0normfnTnormA=normfnifTLinFnContFnT×0normA
6 3 5 breq12d T=ifTLinFnContFnT×0TAnormfnTnormAifTLinFnContFnT×0AnormfnifTLinFnContFnT×0normA
7 6 imbi2d T=ifTLinFnContFnT×0ATAnormfnTnormAAifTLinFnContFnT×0AnormfnifTLinFnContFnT×0normA
8 0lnfn ×0LinFn
9 0cnfn ×0ContFn
10 elin ×0LinFnContFn×0LinFn×0ContFn
11 8 9 10 mpbir2an ×0LinFnContFn
12 11 elimel ifTLinFnContFnT×0LinFnContFn
13 elin ifTLinFnContFnT×0LinFnContFnifTLinFnContFnT×0LinFnifTLinFnContFnT×0ContFn
14 12 13 mpbi ifTLinFnContFnT×0LinFnifTLinFnContFnT×0ContFn
15 14 simpli ifTLinFnContFnT×0LinFn
16 14 simpri ifTLinFnContFnT×0ContFn
17 15 16 nmcfnlbi AifTLinFnContFnT×0AnormfnifTLinFnContFnT×0normA
18 7 17 dedth TLinFnContFnATAnormfnTnormA
19 18 imp TLinFnContFnATAnormfnTnormA
20 1 19 sylanbr TLinFnTContFnATAnormfnTnormA
21 20 3impa TLinFnTContFnATAnormfnTnormA