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