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	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{ContOp}$$

Proof

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