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

Metamath Proof Explorer

Theorem lncnopbd

Description: A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lncnopbd ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ 𝑇 ∈ BndLinOp )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) )
2 lnopcnbd ⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp ) )
3 2 biimpa ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) → 𝑇 ∈ BndLinOp )
4 bdopln ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )
5 2 biimparc ⊢ ( ( 𝑇 ∈ BndLinOp ∧ 𝑇 ∈ LinOp ) → 𝑇 ∈ ContOp )
6 4 5 mpdan ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ ContOp )
7 4 6 jca ⊢ ( 𝑇 ∈ BndLinOp → ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) )
8 3 7 impbii ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) ↔ 𝑇 ∈ BndLinOp )
9 1 8 bitri ⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ 𝑇 ∈ BndLinOp )