# Metamath Proof Explorer

## Theorem hoid1ri

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 hoid1ri ${⊢}{I}_{\mathrm{op}}\circ {T}={T}$

### Proof

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