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