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 )