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

Metamath Proof Explorer

Theorem idunop

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

		Ref	Expression
	Assertion	idunop	$⊢ {I ↾}_{ℋ} \in UniOp$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ$
2		f1ofo	$⊢ ({I ↾}_{ℋ}) : ℋ \underset{1-1 onto}{⟶} ℋ \to ({I ↾}_{ℋ}) : ℋ \underset{onto}{⟶} ℋ$
3	1 2	ax-mp	$⊢ ({I ↾}_{ℋ}) : ℋ \underset{onto}{⟶} ℋ$
4		fvresi	$⊢ x \in ℋ \to ({I ↾}_{ℋ}) (x) = x$
5		fvresi	$⊢ y \in ℋ \to ({I ↾}_{ℋ}) (y) = y$
6	4 5	oveqan12d	$⊢ (x \in ℋ \land y \in ℋ) \to ({I ↾}_{ℋ}) (x) \cdot_{ih} ({I ↾}_{ℋ}) (y) = x \cdot_{ih} y$
7	6	rgen2	$⊢ \forall x \in ℋ \forall y \in ℋ ({I ↾}_{ℋ}) (x) \cdot_{ih} ({I ↾}_{ℋ}) (y) = x \cdot_{ih} y$
8		elunop	$⊢ {I ↾}_{ℋ} \in UniOp \leftrightarrow (({I ↾}_{ℋ}) : ℋ \underset{onto}{⟶} ℋ \land \forall x \in ℋ \forall y \in ℋ ({I ↾}_{ℋ}) (x) \cdot_{ih} ({I ↾}_{ℋ}) (y) = x \cdot_{ih} y)$
9	3 7 8	mpbir2an	$⊢ {I ↾}_{ℋ} \in UniOp$