# Metamath Proof Explorer

## Theorem elpjch

Description: Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion elpjch ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left(\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}\wedge {T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfpjop ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}↔\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)$
2 hmopidmch ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to \mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}$
3 hmopidmpj ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to {T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)$
4 2 3 jca ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to \left(\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}\wedge {T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)\right)$
5 1 4 sylbi ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left(\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}\wedge {T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)\right)$