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

Metamath Proof Explorer

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