# Metamath Proof Explorer

## Theorem hoid1i

Description: Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddid1.1 ${⊢}{T}:ℋ⟶ℋ$
Assertion hoid1i ${⊢}{T}\circ {I}_{\mathrm{op}}={T}$

### Proof

Step Hyp Ref Expression
1 hoaddid1.1 ${⊢}{T}:ℋ⟶ℋ$
2 df-iop ${⊢}{I}_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(ℋ\right)$
3 2 coeq2i ${⊢}{T}\circ {I}_{\mathrm{op}}={T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)$
4 helch ${⊢}ℋ\in {\mathbf{C}}_{ℋ}$
5 4 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right):ℋ⟶ℋ$
6 1 5 hocoi ${⊢}{x}\in ℋ\to \left({T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)\right)\left({x}\right)={T}\left({\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)\right)$
7 pjch1 ${⊢}{x}\in ℋ\to {\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)={x}$
8 7 fveq2d ${⊢}{x}\in ℋ\to {T}\left({\mathrm{proj}}_{ℎ}\left(ℋ\right)\left({x}\right)\right)={T}\left({x}\right)$
9 6 8 eqtrd ${⊢}{x}\in ℋ\to \left({T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)\right)\left({x}\right)={T}\left({x}\right)$
10 9 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)\right)\left({x}\right)={T}\left({x}\right)$
11 1 5 hocofi ${⊢}\left({T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)\right):ℋ⟶ℋ$
12 11 1 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)\right)\left({x}\right)={T}\left({x}\right)↔{T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)={T}$
13 10 12 mpbi ${⊢}{T}\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)={T}$
14 3 13 eqtri ${⊢}{T}\circ {I}_{\mathrm{op}}={T}$