Metamath Proof Explorer

Theorem lnfnconi

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis lnfncon.1 ⊢ T ∈ LinFn
Assertion lnfnconi ⊢ T ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y

Proof

Step Hyp Ref Expression
1 lnfncon.1 ⊢ T ∈ LinFn
2 nmcfnex ⊢ T ∈ LinFn ∧ T ∈ ContFn → norm fn ⁡ T ∈ ℝ
3 1 2 mpan ⊢ T ∈ ContFn → norm fn ⁡ T ∈ ℝ
4 nmcfnlb ⊢ T ∈ LinFn ∧ T ∈ ContFn ∧ y ∈ ℋ → T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
5 1 4 mp3an1 ⊢ T ∈ ContFn ∧ y ∈ ℋ → T ⁡ y ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ y
6 1 lnfnfi ⊢ T : ℋ ⟶ ℂ
7 elcnfn ⊢ T ∈ ContFn ↔ T : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ z ∈ ℝ + ∃ y ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < y → T ⁡ w − T ⁡ x < z
8 6 7 mpbiran ⊢ T ∈ ContFn ↔ ∀ x ∈ ℋ ∀ z ∈ ℝ + ∃ y ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < y → T ⁡ w − T ⁡ x < z
9 6 ffvelrni ⊢ y ∈ ℋ → T ⁡ y ∈ ℂ
10 9 abscld ⊢ y ∈ ℋ → T ⁡ y ∈ ℝ
11 1 lnfnsubi ⊢ w ∈ ℋ ∧ x ∈ ℋ → T ⁡ w - ℎ x = T ⁡ w − T ⁡ x
12 3 5 8 10 11 lnconi ⊢ T ∈ ContFn ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y