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 ↾}_{ℋ} \in ContOp$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ$
2		f1of	$⊢ ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ \to ({I ↾}_{ℋ}) : ℋ ⟶ ℋ$
3	1 2	ax-mp	$⊢ ({I ↾}_{ℋ}) : ℋ ⟶ ℋ$
4		id	$⊢ y \in ℝ^{+} \to y \in ℝ^{+}$
5		fvresi	$⊢ w \in ℋ \to ({I ↾}_{ℋ}) (w) = w$
6		fvresi	$⊢ x \in ℋ \to ({I ↾}_{ℋ}) (x) = x$
7	5 6	oveqan12rd	$⊢ (x \in ℋ \land w \in ℋ) \to ({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x) = w -_{ℎ} x$
8	7	fveq2d	$⊢ (x \in ℋ \land w \in ℋ) \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) = {norm}_{ℎ} (w -_{ℎ} x)$
9	8	breq1d	$⊢ (x \in ℋ \land w \in ℋ) \to ({norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y \leftrightarrow {norm}_{ℎ} (w -_{ℎ} x) < y)$
10	9	biimprd	$⊢ (x \in ℋ \land w \in ℋ) \to ({norm}_{ℎ} (w -_{ℎ} x) < y \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y)$
11	10	ralrimiva	$⊢ x \in ℋ \to \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y)$
12		breq2	$⊢ z = y \to ({norm}_{ℎ} (w -_{ℎ} x) < z \leftrightarrow {norm}_{ℎ} (w -_{ℎ} x) < y)$
13	12	rspceaimv	$⊢ (y \in ℝ^{+} \land \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < y \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y)) \to \exists z \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < z \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y)$
14	4 11 13	syl2anr	$⊢ (x \in ℋ \land y \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < z \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y)$
15	14	rgen2	$⊢ \forall x \in ℋ \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < z \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y)$
16		elcnop	$⊢ {I ↾}_{ℋ} \in ContOp \leftrightarrow (({I ↾}_{ℋ}) : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in ℋ ({norm}_{ℎ} (w -_{ℎ} x) < z \to {norm}_{ℎ} (({I ↾}_{ℋ}) (w) -_{ℎ} ({I ↾}_{ℋ}) (x)) < y))$
17	3 15 16	mpbir2an	$⊢ {I ↾}_{ℋ} \in ContOp$