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 𝐾 ) )