Theorem isblo2

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

	Ref	Expression
Hypotheses	bloval.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	bloval.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	bloval.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion	isblo2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		bloval.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2		bloval.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
3		bloval.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
4	1 2 3	isblo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )
5		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
7	5 6 2	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) )
8	5 6 1	nmoreltpnf	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) < +∞ ) )
9	7 8	syld3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) < +∞ ) )
10	9	3expa	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑇 ∈ 𝐿 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) < +∞ ) )
11	10	pm5.32da	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )
12	4 11	bitr4d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) ) )