This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idcnop

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

Ref Expression
Assertion idcnop ( I ↾ ℋ ) ∈ ContOp

Proof

Step Hyp Ref Expression
1 f1oi ⊢ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ
2 f1of ⊢ ( ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ → ( I ↾ ℋ ) : ℋ ⟶ ℋ )
3 1 2 ax-mp ⊢ ( I ↾ ℋ ) : ℋ ⟶ ℋ
4 id ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ+ )
5 fvresi ⊢ ( 𝑤 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑤 ) = 𝑤 )
6 fvresi ⊢ ( 𝑥 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑥 ) = 𝑥 )
7 5 6 oveqan12rd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) = ( 𝑤 −ℎ 𝑥 ) )
8 7 fveq2d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) = ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) )
9 8 breq1d ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 ) )
10 9 biimprd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ) )
11 10 ralrimiva ⊢ ( 𝑥 ∈ ℋ → ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ) )
12 breq2 ⊢ ( 𝑧 = 𝑦 → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 ) )
13 12 rspceaimv ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ) )
14 4 11 13 syl2anr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ) )
15 14 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 )
16 elcnop ⊢ ( ( I ↾ ℋ ) ∈ ContOp ↔ ( ( I ↾ ℋ ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( normℎ ‘ ( ( ( I ↾ ℋ ) ‘ 𝑤 ) −ℎ ( ( I ↾ ℋ ) ‘ 𝑥 ) ) ) < 𝑦 ) ) )
17 3 15 16 mpbir2an ⊢ ( I ↾ ℋ ) ∈ ContOp