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

Metamath Proof Explorer

Theorem hoif

Description: Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hoif	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ$

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ$
2		dfiop2	$⊢ I_{op} = {I ↾}_{ℋ}$
3		f1oeq1	$⊢ I_{op} = {I ↾}_{ℋ} \to (I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ \leftrightarrow ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ)$
4	2 3	ax-mp	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ \leftrightarrow ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ$
5	1 4	mpbir	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ$