Metamath Proof Explorer

Theorem 0cnfn

Description: The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0cnfn ⊢ ℋ × 0 ∈ ContFn

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 1 fconst6 ⊢ ℋ × 0 : ℋ ⟶ ℂ
3 1rp ⊢ 1 ∈ ℝ +
4 c0ex ⊢ 0 ∈ V
5 4 fvconst2 ⊢ w ∈ ℋ → ℋ × 0 ⁡ w = 0
6 4 fvconst2 ⊢ x ∈ ℋ → ℋ × 0 ⁡ x = 0
7 5 6 oveqan12rd ⊢ x ∈ ℋ ∧ w ∈ ℋ → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x = 0 − 0
8 7 adantlr ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x = 0 − 0
9 0m0e0 ⊢ 0 − 0 = 0
10 8 9 eqtrdi ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x = 0
11 10 fveq2d ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x = 0
12 abs0 ⊢ 0 = 0
13 11 12 eqtrdi ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x = 0
14 rpgt0 ⊢ y ∈ ℝ + → 0 < y
15 14 ad2antlr ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → 0 < y
16 13 15 eqbrtrd ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
17 16 a1d ⊢ x ∈ ℋ ∧ y ∈ ℝ + ∧ w ∈ ℋ → norm ℎ ⁡ w - ℎ x < 1 → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
18 17 ralrimiva ⊢ x ∈ ℋ ∧ y ∈ ℝ + → ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < 1 → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
19 breq2 ⊢ z = 1 → norm ℎ ⁡ w - ℎ x < z ↔ norm ℎ ⁡ w - ℎ x < 1
20 19 rspceaimv ⊢ 1 ∈ ℝ + ∧ ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < 1 → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y → ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
21 3 18 20 sylancr ⊢ x ∈ ℋ ∧ y ∈ ℝ + → ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
22 21 rgen2 ⊢ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
23 elcnfn ⊢ ℋ × 0 ∈ ContFn ↔ ℋ × 0 : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → ℋ × 0 ⁡ w − ℋ × 0 ⁡ x < y
24 2 22 23 mpbir2an ⊢ ℋ × 0 ∈ ContFn