nmoreltpnf

Description: The norm of any operator is real iff it is less than plus 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	nmoreltpnf	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to (N (T) \in ℝ \leftrightarrow 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	1 2 3	nmoxr	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to N (T) \in ℝ^{*}$
6		nltpnft	$⊢ N (T) \in ℝ^{*} \to (N (T) = +∞ \leftrightarrow \neg N (T) < +∞)$
7	5 6	syl	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to (N (T) = +∞ \leftrightarrow \neg N (T) < +∞)$
8	7	necon2abid	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to (N (T) < +∞ \leftrightarrow N (T) \neq +∞)$
9	4 8	bitr4d	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T : X ⟶ Y) \to (N (T) \in ℝ \leftrightarrow N (T) < +∞)$

Metamath Proof Explorer