This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ ) ) )