Metamath Proof Explorer

Theorem 0cnop

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

Ref Expression
Assertion 0cnop 0hop ∈ ContOp

Proof

Step Hyp Ref Expression
1 ho0f ⊢ 0hop : ℋ ⟶ ℋ
2 1rp ⊢ 1 ∈ ℝ+
3 ho0val ⊢ ( 𝑤 ∈ ℋ → ( 0hop ‘ 𝑤 ) = 0ℎ )
4 ho0val ⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
5 3 4 oveqan12rd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) = ( 0ℎ −ℎ 0ℎ ) )
6 5 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) = ( 0ℎ −ℎ 0ℎ ) )
7 ax-hv0cl ⊢ 0ℎ ∈ ℋ
8 hvsubid ⊢ ( 0ℎ ∈ ℋ → ( 0ℎ −ℎ 0ℎ ) = 0ℎ )
9 7 8 ax-mp ⊢ ( 0ℎ −ℎ 0ℎ ) = 0ℎ
10 6 9 eqtrdi ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) = 0ℎ )
11 10 fveq2d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) = ( normℎ ‘ 0ℎ ) )
12 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
13 11 12 eqtrdi ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) = 0 )
14 rpgt0 ⊢ ( 𝑦 ∈ ℝ+ → 0 < 𝑦 )
15 14 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → 0 < 𝑦 )
16 13 15 eqbrtrd ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 )
17 16 a1d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 ) )
18 17 ralrimiva ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 ) )
19 breq2 ⊢ ( 𝑧 = 1 → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 ) )
20 19 rspceaimv ⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 1 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 ) )
21 2 18 20 sylancr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 ) )
22 21 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 )
23 elcnop ⊢ ( 0hop ∈ ContOp ↔ ( 0hop : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( 0hop ‘ 𝑤 ) −ℎ ( 0hop ‘ 𝑥 ) ) ) < 𝑦 ) ) )
24 1 22 23 mpbir2an ⊢ 0hop ∈ ContOp