Theorem 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	⊢ 𝑍 = ( 𝑈 0op 𝑊 )
	0blo.7	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion	0blo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		0blo.0	⊢ 𝑍 = ( 𝑈 0op 𝑊 )
2		0blo.7	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
3		eqid	⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
4	1 3	0lno	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 ∈ ( 𝑈 LnOp 𝑊 ) )
5		eqid	⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
6	5 1	nmoo0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑍 ) = 0 )
7		0re	⊢ 0 ∈ ℝ
8	6 7	eqeltrdi	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑍 ) ∈ ℝ )
9	5 3 2	isblo2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑍 ∈ 𝐵 ↔ ( 𝑍 ∈ ( 𝑈 LnOp 𝑊 ) ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑍 ) ∈ ℝ ) ) )
10	4 8 9	mpbir2and	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 ∈ 𝐵 )