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

Metamath Proof Explorer

Theorem blocn2

Description: A bounded linear operator is continuous. (Contributed by NM, 25-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses blocn.8 ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
blocn.d ⊢ 𝐷 = ( IndMet ‘ 𝑊 )
blocn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
blocn.k ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
blocn.5 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
blocn.u ⊢ 𝑈 ∈ NrmCVec
blocn.w ⊢ 𝑊 ∈ NrmCVec
Assertion blocn2 ( 𝑇 ∈ 𝐵 → 𝑇 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 blocn.8 ⊢ 𝐶 = ( IndMet ‘ 𝑈 )
2 blocn.d ⊢ 𝐷 = ( IndMet ‘ 𝑊 )
3 blocn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
4 blocn.k ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
5 blocn.5 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6 blocn.u ⊢ 𝑈 ∈ NrmCVec
7 blocn.w ⊢ 𝑊 ∈ NrmCVec
8 eqid ⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
9 8 5 bloln ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
10 6 7 9 mp3an12 ⊢ ( 𝑇 ∈ 𝐵 → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
11 1 2 3 4 5 6 7 8 blocn ⊢ ( 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) → ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇 ∈ 𝐵 ) )
12 11 biimprd ⊢ ( 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) → ( 𝑇 ∈ 𝐵 → 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ) )
13 10 12 mpcom ⊢ ( 𝑇 ∈ 𝐵 → 𝑇 ∈ ( 𝐽 Cn 𝐾 ) )