Theorem nmfnrepnf

Description: The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	nmfnrepnf	|- ( T : ~H --> CC -> ( ( normfn ` T ) e. RR <-> ( normfn ` T ) =/= +oo ) )

Proof

Step	Hyp	Ref	Expression
1		nmfnsetre	|- ( T : ~H --> CC -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } C_ RR )
2		nmfnsetn0	|- ( abs ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) }
3	2	ne0ii	|- { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } =/= (/)
4		supxrre2	|- ( ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } C_ RR /\ { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } =/= (/) ) -> ( sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) e. RR <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) =/= +oo ) )
5	1 3 4	sylancl	|- ( T : ~H --> CC -> ( sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) e. RR <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) =/= +oo ) )
6		nmfnval	|- ( T : ~H --> CC -> ( normfn ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) )
7	6	eleq1d	|- ( T : ~H --> CC -> ( ( normfn ` T ) e. RR <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) e. RR ) )
8	6	neeq1d	|- ( T : ~H --> CC -> ( ( normfn ` T ) =/= +oo <-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } , RR* , < ) =/= +oo ) )
9	5 7 8	3bitr4d	|- ( T : ~H --> CC -> ( ( normfn ` T ) e. RR <-> ( normfn ` T ) =/= +oo ) )