Metamath Proof Explorer

Theorem nmcfnex

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

Ref Expression
Assertion nmcfnex 
|- ( ( T e. LinFn /\ T e. ContFn ) -> ( normfn ` T ) e. RR )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( T e. ( LinFn i^i ContFn ) <-> ( T e. LinFn /\ T e. ContFn ) )
2 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 } ) ) ) )
3 2 eleq1d 
 |-  ( T = if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) -> ( ( normfn ` T ) e. RR <-> ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) e. RR ) )
4 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
5 0cnfn 
 |-  ( ~H X. { 0 } ) e. ContFn
6 elin 
 |-  ( ( ~H X. { 0 } ) e. ( LinFn i^i ContFn ) <-> ( ( ~H X. { 0 } ) e. LinFn /\ ( ~H X. { 0 } ) e. ContFn ) )
7 4 5 6 mpbir2an 
 |-  ( ~H X. { 0 } ) e. ( LinFn i^i ContFn )
8 7 elimel 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ( LinFn i^i ContFn )
9 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 ) )
10 8 9 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 )
11 10 simpli 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. LinFn
12 10 simpri 
 |-  if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) e. ContFn
13 11 12 nmcfnexi 
 |-  ( normfn ` if ( T e. ( LinFn i^i ContFn ) , T , ( ~H X. { 0 } ) ) ) e. RR
14 3 13 dedth 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( normfn ` T ) e. RR )
15 1 14 sylbir 
 |-  ( ( T e. LinFn /\ T e. ContFn ) -> ( normfn ` T ) e. RR )