# Metamath Proof Explorer

## Theorem dfiop2

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

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

### Proof

Step Hyp Ref Expression
1 df-iop ${⊢}{I}_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(ℋ\right)$
2 helch ${⊢}ℋ\in {\mathbf{C}}_{ℋ}$
3 2 pjfni ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right)Fnℋ$
4 fnresi ${⊢}\left({\mathrm{I}↾}_{ℋ}\right)Fnℋ$
5 pjch1 ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)={x}$
6 fvresi ${⊢}{x}\in ℋ\to \left({\mathrm{I}↾}_{ℋ}\right)\left({x}\right)={x}$
7 5 6 eqtr4d ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)=\left({\mathrm{I}↾}_{ℋ}\right)\left({x}\right)$
8 7 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)=\left({\mathrm{I}↾}_{ℋ}\right)\left({x}\right)$
9 eqfnfv ${⊢}\left({\mathrm{proj}}_{ℎ}\left(ℋ\right)Fnℋ\wedge \left({\mathrm{I}↾}_{ℋ}\right)Fnℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left(ℋ\right)={\mathrm{I}↾}_{ℋ}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)=\left({\mathrm{I}↾}_{ℋ}\right)\left({x}\right)\right)$
10 8 9 mpbiri ${⊢}\left({\mathrm{proj}}_{ℎ}\left(ℋ\right)Fnℋ\wedge \left({\mathrm{I}↾}_{ℋ}\right)Fnℋ\right)\to {\mathrm{proj}}_{ℎ}\left(ℋ\right)={\mathrm{I}↾}_{ℋ}$
11 3 4 10 mp2an ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right)={\mathrm{I}↾}_{ℋ}$
12 1 11 eqtri ${⊢}{I}_{\mathrm{op}}={\mathrm{I}↾}_{ℋ}$