Metamath Proof Explorer

Theorem nmopgtmnf

Description: The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopgtmnf
`|- ( T : ~H --> ~H -> -oo < ( normop ` T ) )`

Proof

Step Hyp Ref Expression
1 nmoprepnf
` |-  ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> ( normop ` T ) =/= +oo ) )`
2 df-ne
` |-  ( ( normop ` T ) =/= +oo <-> -. ( normop ` T ) = +oo )`
3 1 2 syl6bb
` |-  ( T : ~H --> ~H -> ( ( normop ` T ) e. RR <-> -. ( normop ` T ) = +oo ) )`
4 xor3
` |-  ( -. ( ( normop ` T ) e. RR <-> ( normop ` T ) = +oo ) <-> ( ( normop ` T ) e. RR <-> -. ( normop ` T ) = +oo ) )`
5 nbior
` |-  ( -. ( ( normop ` T ) e. RR <-> ( normop ` T ) = +oo ) -> ( ( normop ` T ) e. RR \/ ( normop ` T ) = +oo ) )`
6 4 5 sylbir
` |-  ( ( ( normop ` T ) e. RR <-> -. ( normop ` T ) = +oo ) -> ( ( normop ` T ) e. RR \/ ( normop ` T ) = +oo ) )`
7 mnfltxr
` |-  ( ( ( normop ` T ) e. RR \/ ( normop ` T ) = +oo ) -> -oo < ( normop ` T ) )`
8 3 6 7 3syl
` |-  ( T : ~H --> ~H -> -oo < ( normop ` T ) )`