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 = BaseSet (U)$
	nmoxr.2	$⊢ Y = BaseSet (W)$
	nmoxr.3	$⊢ N = U {normOp}_{OLD} W$
Assertion	nmogtmnf	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to −∞ < N (T)$

Step	Hyp	Ref	Expression
1		nmoxr.1	$⊢ X = BaseSet (U)$
2		nmoxr.2	$⊢ Y = BaseSet (W)$
3		nmoxr.3	$⊢ N = U {normOp}_{OLD} W$
4	1 2 3	nmorepnf	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to (N (T) \in ℝ \leftrightarrow N (T) \neq +∞)$
5		df-ne	$⊢ N (T) \neq +∞ \leftrightarrow \neg N (T) = +∞$
6	4 5	bitrdi	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to (N (T) \in ℝ \leftrightarrow \neg N (T) = +∞)$
7		xor3	$⊢ \neg (N (T) \in ℝ \leftrightarrow N (T) = +∞) \leftrightarrow (N (T) \in ℝ \leftrightarrow \neg N (T) = +∞)$
8		nbior	$⊢ \neg (N (T) \in ℝ \leftrightarrow N (T) = +∞) \to (N (T) \in ℝ \lor N (T) = +∞)$
9	7 8	sylbir	$⊢ (N (T) \in ℝ \leftrightarrow \neg N (T) = +∞) \to (N (T) \in ℝ \lor N (T) = +∞)$
10		mnfltxr	$⊢ (N (T) \in ℝ \lor N (T) = +∞) \to −∞ < N (T)$
11	6 9 10	3syl	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to −∞ < N (T)$

Metamath Proof Explorer