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 ‘ 𝑇 ) ∈ ℝ ) )