Metamath Proof Explorer

Theorem nmcoplb

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

Ref Expression
Assertion nmcoplb 
|- ( ( T e. LinOp /\ T e. ContOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( T e. ( LinOp i^i ContOp ) <-> ( T e. LinOp /\ T e. ContOp ) )
2 fveq1 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( T ` A ) = ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ` A ) )
3 2 fveq2d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( normh ` ( T ` A ) ) = ( normh ` ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ` A ) ) )
4 fveq2 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( normop ` T ) = ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) )
5 4 oveq1d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( ( normop ` T ) x. ( normh ` A ) ) = ( ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) x. ( normh ` A ) ) )
6 3 5 breq12d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) <-> ( normh ` ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ` A ) ) <_ ( ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) x. ( normh ` A ) ) ) )
7 6 imbi2d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) ) <-> ( A e. ~H -> ( normh ` ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ` A ) ) <_ ( ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) x. ( normh ` A ) ) ) ) )
8 idlnop 
 |-  ( _I |` ~H ) e. LinOp
9 idcnop 
 |-  ( _I |` ~H ) e. ContOp
10 elin 
 |-  ( ( _I |` ~H ) e. ( LinOp i^i ContOp ) <-> ( ( _I |` ~H ) e. LinOp /\ ( _I |` ~H ) e. ContOp ) )
11 8 9 10 mpbir2an 
 |-  ( _I |` ~H ) e. ( LinOp i^i ContOp )
12 11 elimel 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ( LinOp i^i ContOp )
13 elin 
 |-  ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ( LinOp i^i ContOp ) <-> ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. LinOp /\ if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ContOp ) )
14 12 13 mpbi 
 |-  ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. LinOp /\ if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ContOp )
15 14 simpli 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. LinOp
16 14 simpri 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ContOp
17 15 16 nmcoplbi 
 |-  ( A e. ~H -> ( normh ` ( if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ` A ) ) <_ ( ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) x. ( normh ` A ) ) )
18 7 17 dedth 
 |-  ( T e. ( LinOp i^i ContOp ) -> ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) ) )
19 18 imp 
 |-  ( ( T e. ( LinOp i^i ContOp ) /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
20 1 19 sylanbr 
 |-  ( ( ( T e. LinOp /\ T e. ContOp ) /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
21 20 3impa 
 |-  ( ( T e. LinOp /\ T e. ContOp /\ A e. ~H ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )