# Metamath Proof Explorer

## Theorem nmogtmnf

Description: The norm of an operator is greater than minus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nmoxr.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
nmoxr.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
Assertion nmogtmnf ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \mathrm{-\infty }<{N}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 nmoxr.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nmoxr.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 nmoxr.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
4 1 2 3 nmorepnf ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)\ne \mathrm{+\infty }\right)$
5 df-ne ${⊢}{N}\left({T}\right)\ne \mathrm{+\infty }↔¬{N}\left({T}\right)=\mathrm{+\infty }$
6 4 5 syl6bb ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \left({N}\left({T}\right)\in ℝ↔¬{N}\left({T}\right)=\mathrm{+\infty }\right)$
7 xor3 ${⊢}¬\left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)=\mathrm{+\infty }\right)↔\left({N}\left({T}\right)\in ℝ↔¬{N}\left({T}\right)=\mathrm{+\infty }\right)$
8 nbior ${⊢}¬\left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)=\mathrm{+\infty }\right)\to \left({N}\left({T}\right)\in ℝ\vee {N}\left({T}\right)=\mathrm{+\infty }\right)$
9 7 8 sylbir ${⊢}\left({N}\left({T}\right)\in ℝ↔¬{N}\left({T}\right)=\mathrm{+\infty }\right)\to \left({N}\left({T}\right)\in ℝ\vee {N}\left({T}\right)=\mathrm{+\infty }\right)$
10 mnfltxr ${⊢}\left({N}\left({T}\right)\in ℝ\vee {N}\left({T}\right)=\mathrm{+\infty }\right)\to \mathrm{-\infty }<{N}\left({T}\right)$
11 6 9 10 3syl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:{X}⟶{Y}\right)\to \mathrm{-\infty }<{N}\left({T}\right)$