Theorem lnopcnbd

Description: A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	lnopcnbd	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp ) )

Proof

Step	Hyp	Ref	Expression
1		nmcopex	⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
2	1	ex	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp → ( normop ‘ 𝑇 ) ∈ ℝ ) )
3		elbdop2	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) )
4	3	baibr	⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ 𝑇 ∈ BndLinOp ) )
5	2 4	sylibd	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp → 𝑇 ∈ BndLinOp ) )
6		nmopre	⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
7		nmbdoplb	⊢ ( ( 𝑇 ∈ BndLinOp ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
8	7	ralrimiva	⊢ ( 𝑇 ∈ BndLinOp → ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
9		oveq1	⊢ ( 𝑥 = ( normop ‘ 𝑇 ) → ( 𝑥 · ( normℎ ‘ 𝑦 ) ) = ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
10	9	breq2d	⊢ ( 𝑥 = ( normop ‘ 𝑇 ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) )
11	10	ralbidv	⊢ ( 𝑥 = ( normop ‘ 𝑇 ) → ( ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) )
12	11	rspcev	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
13	6 8 12	syl2anc	⊢ ( 𝑇 ∈ BndLinOp → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
14		lnopcon	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )
15	13 14	imbitrrid	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ BndLinOp → 𝑇 ∈ ContOp ) )
16	5 15	impbid	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp ) )