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 ⊢ T ∈ LinFn → T ∈ ContFn ↔ norm fn ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 nmcfnex ⊢ T ∈ LinFn ∧ T ∈ ContFn → norm fn ⁡ T ∈ ℝ
2 1 ex ⊢ T ∈ LinFn → T ∈ ContFn → norm fn ⁡ T ∈ ℝ
3 simpr ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ → norm fn ⁡ T ∈ ℝ
4 nmbdfnlb ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ ∧ y ∈ ℋ → T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
5 4 3expa ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ ∧ y ∈ ℋ → T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
6 5 ralrimiva ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ → ∀ y ∈ ℋ T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
7 oveq1 ⊢ x = norm fn ⁡ T → x ⁢ norm ℎ ⁡ y = norm fn ⁡ T ⁢ norm ℎ ⁡ y
8 7 breq2d ⊢ x = norm fn ⁡ T → T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
9 8 ralbidv ⊢ x = norm fn ⁡ T → ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y ↔ ∀ y ∈ ℋ T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
10 9 rspcev ⊢ norm fn ⁡ T ∈ ℝ ∧ ∀ y ∈ ℋ T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y → ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
11 3 6 10 syl2anc ⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ → ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
12 11 ex ⊢ T ∈ LinFn → norm fn ⁡ T ∈ ℝ → ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
13 lnfncon ⊢ T ∈ LinFn → T ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y
14 12 13 sylibrd ⊢ T ∈ LinFn → norm fn ⁡ T ∈ ℝ → T ∈ ContFn
15 2 14 impbid ⊢ T ∈ LinFn → T ∈ ContFn ↔ norm fn ⁡ T ∈ ℝ