Metamath Proof Explorer

Theorem nmbdfnlb

Description: A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion nmbdfnlb 
|- ( ( T e. LinFn /\ ( normfn ` T ) e. RR /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( T ` A ) = ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ` A ) )
2 1 fveq2d 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( abs ` ( T ` A ) ) = ( abs ` ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ` A ) ) )
3 fveq2 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( normfn ` T ) = ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) )
4 3 oveq1d 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( normfn ` T ) x. ( normh ` A ) ) = ( ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) )
5 2 4 breq12d 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) <-> ( abs ` ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ` A ) ) <_ ( ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) ) )
6 5 imbi2d 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) <-> ( A e. ~H -> ( abs ` ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ` A ) ) <_ ( ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) ) ) )
7 eleq1 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( T e. LinFn <-> if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) e. LinFn ) )
8 3 eleq1d 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( normfn ` T ) e. RR <-> ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) e. RR ) )
9 7 8 anbi12d 
 |-  ( T = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) <-> ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) e. LinFn /\ ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) e. RR ) ) )
10 eleq1 
 |-  ( ( ~H X. { 0 } ) = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( ~H X. { 0 } ) e. LinFn <-> if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) e. LinFn ) )
11 fveq2 
 |-  ( ( ~H X. { 0 } ) = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( normfn ` ( ~H X. { 0 } ) ) = ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) )
12 11 eleq1d 
 |-  ( ( ~H X. { 0 } ) = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( normfn ` ( ~H X. { 0 } ) ) e. RR <-> ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) e. RR ) )
13 10 12 anbi12d 
 |-  ( ( ~H X. { 0 } ) = if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) -> ( ( ( ~H X. { 0 } ) e. LinFn /\ ( normfn ` ( ~H X. { 0 } ) ) e. RR ) <-> ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) e. LinFn /\ ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) e. RR ) ) )
14 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
15 nmfn0 
 |-  ( normfn ` ( ~H X. { 0 } ) ) = 0
16 0re 
 |-  0 e. RR
17 15 16 eqeltri 
 |-  ( normfn ` ( ~H X. { 0 } ) ) e. RR
18 14 17 pm3.2i 
 |-  ( ( ~H X. { 0 } ) e. LinFn /\ ( normfn ` ( ~H X. { 0 } ) ) e. RR )
19 9 13 18 elimhyp 
 |-  ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) e. LinFn /\ ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) e. RR )
20 19 nmbdfnlbi 
 |-  ( A e. ~H -> ( abs ` ( if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ` A ) ) <_ ( ( normfn ` if ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) )
21 6 20 dedth 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
22 21 3impia 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )