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 
|- ( ( T e. LinFn /\ T e. ContFn /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( T e. ( LinFn i^i ContFn ) <-> ( T e. LinFn /\ T e. ContFn ) )
2 fveq1 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( T ` A ) = ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` A ) )
3 2 fveq2d 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( abs ` ( T ` A ) ) = ( abs ` ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` A ) ) )
4 fveq2 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( normfn ` T ) = ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) )
5 4 oveq1d 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( ( normfn ` T ) x. ( normh ` A ) ) = ( ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) )
6 3 5 breq12d 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) <-> ( abs ` ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` A ) ) <_ ( ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) ) )
7 6 imbi2d 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) <-> ( A e. ~H -> ( abs ` ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` A ) ) <_ ( ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) ) ) )
8 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
9 0cnfn 
 |-  ( ~H X. { 0 } ) e. ContFn
10 elin 
 |-  ( ( ~H X. { 0 } ) e. ( LinFn i^i ContFn ) <-> ( ( ~H X. { 0 } ) e. LinFn /\ ( ~H X. { 0 } ) e. ContFn ) )
11 8 9 10 mpbir2an 
 |-  ( ~H X. { 0 } ) e. ( LinFn i^i ContFn )
12 11 elimel 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ( LinFn i^i ContFn )
13 elin 
 |-  ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ( LinFn i^i ContFn ) <-> ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. LinFn /\ if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ContFn ) )
14 12 13 mpbi 
 |-  ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. LinFn /\ if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ContFn )
15 14 simpli 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. LinFn
16 14 simpri 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ContFn
17 15 16 nmcfnlbi 
 |-  ( A e. ~H -> ( abs ` ( if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ` A ) ) <_ ( ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) x. ( normh ` A ) ) )
18 7 17 dedth 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
19 18 imp 
 |-  ( ( T e. ( LinFn i^i ContFn ) /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
20 1 19 sylanbr 
 |-  ( ( ( T e. LinFn /\ T e. ContFn ) /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
21 20 3impa 
 |-  ( ( T e. LinFn /\ T e. ContFn /\ A e. ~H ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )