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

Metamath Proof Explorer

Theorem lnfncnbd

Description: A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfncnbd ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ( normfn ‘ 𝑇 ) ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 nmcfnex ⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) → ( normfn ‘ 𝑇 ) ∈ ℝ )
2 1 ex ⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn → ( normfn ‘ 𝑇 ) ∈ ℝ ) )
3 simpr ⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) → ( normfn ‘ 𝑇 ) ∈ ℝ )
4 nmbdfnlb ⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
5 4 3expa ⊢ ( ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
6 5 ralrimiva ⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) → ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
7 oveq1 ⊢ ( 𝑥 = ( normfn ‘ 𝑇 ) → ( 𝑥 · ( normℎ ‘ 𝑦 ) ) = ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
8 7 breq2d ⊢ ( 𝑥 = ( normfn ‘ 𝑇 ) → ( ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) )
9 8 ralbidv ⊢ ( 𝑥 = ( normfn ‘ 𝑇 ) → ( ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) )
10 9 rspcev ⊢ ( ( ( normfn ‘ 𝑇 ) ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
11 3 6 10 syl2anc ⊢ ( ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
12 11 ex ⊢ ( 𝑇 ∈ LinFn → ( ( normfn ‘ 𝑇 ) ∈ ℝ → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )
13 lnfncon ⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) )
14 12 13 sylibrd ⊢ ( 𝑇 ∈ LinFn → ( ( normfn ‘ 𝑇 ) ∈ ℝ → 𝑇 ∈ ContFn ) )
15 2 14 impbid ⊢ ( 𝑇 ∈ LinFn → ( 𝑇 ∈ ContFn ↔ ( normfn ‘ 𝑇 ) ∈ ℝ ) )