This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmcopex

Description: The norm of a continuous linear Hilbert space operator exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmcopex 
|- ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( T e. ( LinOp i^i ContOp ) <-> ( T e. LinOp /\ T e. ContOp ) )
2 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 ) ) ) )
3 2 eleq1d 
 |-  ( T = if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) -> ( ( normop ` T ) e. RR <-> ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) e. RR ) )
4 idlnop 
 |-  ( _I |` ~H ) e. LinOp
5 idcnop 
 |-  ( _I |` ~H ) e. ContOp
6 elin 
 |-  ( ( _I |` ~H ) e. ( LinOp i^i ContOp ) <-> ( ( _I |` ~H ) e. LinOp /\ ( _I |` ~H ) e. ContOp ) )
7 4 5 6 mpbir2an 
 |-  ( _I |` ~H ) e. ( LinOp i^i ContOp )
8 7 elimel 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ( LinOp i^i ContOp )
9 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 ) )
10 8 9 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 )
11 10 simpli 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. LinOp
12 10 simpri 
 |-  if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) e. ContOp
13 11 12 nmcopexi 
 |-  ( normop ` if ( T e. ( LinOp i^i ContOp ) , T , ( _I |` ~H ) ) ) e. RR
14 3 13 dedth 
 |-  ( T e. ( LinOp i^i ContOp ) -> ( normop ` T ) e. RR )
15 1 14 sylbir 
 |-  ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR )