0blo

Description: The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0blo.0	$⊢ Z = U 0_{op} W$
	0blo.7	$⊢ B = U BLnOp W$
Assertion	0blo	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z \in B$

Step	Hyp	Ref	Expression
1		0blo.0	$⊢ Z = U 0_{op} W$
2		0blo.7	$⊢ B = U BLnOp W$
3		eqid	$⊢ U LnOp W = U LnOp W$
4	1 3	0lno	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z \in (U LnOp W)$
5		eqid	$⊢ U {normOp}_{OLD} W = U {normOp}_{OLD} W$
6	5 1	nmoo0	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (U {normOp}_{OLD} W) (Z) = 0$
7		0re	$⊢ 0 \in ℝ$
8	6 7	eqeltrdi	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (U {normOp}_{OLD} W) (Z) \in ℝ$
9	5 3 2	isblo2	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (Z \in B \leftrightarrow (Z \in (U LnOp W) \land (U {normOp}_{OLD} W) (Z) \in ℝ))$
10	4 8 9	mpbir2and	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z \in B$

Metamath Proof Explorer