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 ⊢ ( 𝑤 ∈ ℋ → ( ( ℋ × { 0 } ) ‘ 𝑤 ) = 0 )
6 4 fvconst2 ⊢ ( 𝑥 ∈ ℋ → ( ( ℋ × { 0 } ) ‘ 𝑥 ) = 0 )
7 5 6 oveqan12rd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) = ( 0 − 0 ) )
8 7 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) = ( 0 − 0 ) )
9 0m0e0 ⊢ ( 0 − 0 ) = 0
10 8 9 eqtrdi ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) = 0 )
11 10 fveq2d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) = ( abs ‘ 0 ) )
12 abs0 ⊢ ( abs ‘ 0 ) = 0
13 11 12 eqtrdi ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) = 0 )
14 rpgt0 ⊢ ( 𝑦 ∈ ℝ+ → 0 < 𝑦 )
15 14 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → 0 < 𝑦 )
16 13 15 eqbrtrd ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 )
17 16 a1d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 ) )
18 17 ralrimiva ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 ) )
19 breq2 ⊢ ( 𝑧 = 1 → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 ) )
20 19 rspceaimv ⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 ) )
21 3 18 20 sylancr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 ) )
22 21 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 )
23 elcnfn ⊢ ( ( ℋ × { 0 } ) ∈ ContFn ↔ ( ( ℋ × { 0 } ) : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( ℋ × { 0 } ) ‘ 𝑤 ) − ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
24 2 22 23 mpbir2an ⊢ ( ℋ × { 0 } ) ∈ ContFn