dfiop2

Description: Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	dfiop2	$⊢ I_{op} = {I ↾}_{ℋ}$

Step	Hyp	Ref	Expression
1		df-iop	$⊢ I_{op} = {proj}_{ℎ} (ℋ)$
2		helch	$⊢ ℋ \in C_{ℋ}$
3	2	pjfni	$⊢ {proj}_{ℎ} (ℋ) Fn ℋ$
4		fnresi	$⊢ ({I ↾}_{ℋ}) Fn ℋ$
5		pjch1	$⊢ x \in ℋ \to {proj}_{ℎ} (ℋ) (x) = x$
6		fvresi	$⊢ x \in ℋ \to ({I ↾}_{ℋ}) (x) = x$
7	5 6	eqtr4d	$⊢ x \in ℋ \to {proj}_{ℎ} (ℋ) (x) = ({I ↾}_{ℋ}) (x)$
8	7	rgen	$⊢ \forall x \in ℋ {proj}_{ℎ} (ℋ) (x) = ({I ↾}_{ℋ}) (x)$
9		eqfnfv	$⊢ ({proj}_{ℎ} (ℋ) Fn ℋ \land ({I ↾}_{ℋ}) Fn ℋ) \to ({proj}_{ℎ} (ℋ) = {I ↾}_{ℋ} \leftrightarrow \forall x \in ℋ {proj}_{ℎ} (ℋ) (x) = ({I ↾}_{ℋ}) (x))$
10	8 9	mpbiri	$⊢ ({proj}_{ℎ} (ℋ) Fn ℋ \land ({I ↾}_{ℋ}) Fn ℋ) \to {proj}_{ℎ} (ℋ) = {I ↾}_{ℋ}$
11	3 4 10	mp2an	$⊢ {proj}_{ℎ} (ℋ) = {I ↾}_{ℋ}$
12	1 11	eqtri	$⊢ I_{op} = {I ↾}_{ℋ}$

Metamath Proof Explorer