# Metamath Proof Explorer

## Theorem elpjrn

Description: Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Assertion elpjrn ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \mathrm{ran}{T}=\left\{{x}\in ℋ|{T}\left({x}\right)={x}\right\}$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 simpld ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}$
3 chss ${⊢}\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}\to \mathrm{ran}{T}\subseteq ℋ$
4 2 3 syl ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \mathrm{ran}{T}\subseteq ℋ$
5 4 sseld ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left({x}\in \mathrm{ran}{T}\to {x}\in ℋ\right)$
6 elpjhmop ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {T}\in \mathrm{HrmOp}$
7 hmopf ${⊢}{T}\in \mathrm{HrmOp}\to {T}:ℋ⟶ℋ$
8 6 7 syl ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {T}:ℋ⟶ℋ$
9 8 ffnd ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {T}Fnℋ$
10 fvelrnb ${⊢}{T}Fnℋ\to \left({x}\in \mathrm{ran}{T}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}\right)$
11 9 10 syl ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left({x}\in \mathrm{ran}{T}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}\right)$
12 fvco3 ${⊢}\left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to \left({T}\circ {T}\right)\left({y}\right)={T}\left({T}\left({y}\right)\right)$
13 8 12 sylan ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {y}\in ℋ\right)\to \left({T}\circ {T}\right)\left({y}\right)={T}\left({T}\left({y}\right)\right)$
14 elpjidm ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {T}\circ {T}={T}$
15 14 adantr ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {y}\in ℋ\right)\to {T}\circ {T}={T}$
16 15 fveq1d ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {y}\in ℋ\right)\to \left({T}\circ {T}\right)\left({y}\right)={T}\left({y}\right)$
17 13 16 eqtr3d ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {y}\in ℋ\right)\to {T}\left({T}\left({y}\right)\right)={T}\left({y}\right)$
18 fveq2 ${⊢}{T}\left({y}\right)={x}\to {T}\left({T}\left({y}\right)\right)={T}\left({x}\right)$
19 id ${⊢}{T}\left({y}\right)={x}\to {T}\left({y}\right)={x}$
20 18 19 eqeq12d ${⊢}{T}\left({y}\right)={x}\to \left({T}\left({T}\left({y}\right)\right)={T}\left({y}\right)↔{T}\left({x}\right)={x}\right)$
21 17 20 syl5ibcom ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {y}\in ℋ\right)\to \left({T}\left({y}\right)={x}\to {T}\left({x}\right)={x}\right)$
22 21 rexlimdva ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={x}\to {T}\left({x}\right)={x}\right)$
23 11 22 sylbid ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left({x}\in \mathrm{ran}{T}\to {T}\left({x}\right)={x}\right)$
24 5 23 jcad ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left({x}\in \mathrm{ran}{T}\to \left({x}\in ℋ\wedge {T}\left({x}\right)={x}\right)\right)$
25 fnfvelrn ${⊢}\left({T}Fnℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in \mathrm{ran}{T}$
26 9 25 sylan ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in \mathrm{ran}{T}$
27 eleq1 ${⊢}{T}\left({x}\right)={x}\to \left({T}\left({x}\right)\in \mathrm{ran}{T}↔{x}\in \mathrm{ran}{T}\right)$
28 26 27 syl5ibcom ${⊢}\left({T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\wedge {x}\in ℋ\right)\to \left({T}\left({x}\right)={x}\to {x}\in \mathrm{ran}{T}\right)$
29 28 expimpd ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left(\left({x}\in ℋ\wedge {T}\left({x}\right)={x}\right)\to {x}\in \mathrm{ran}{T}\right)$
30 24 29 impbid ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \left({x}\in \mathrm{ran}{T}↔\left({x}\in ℋ\wedge {T}\left({x}\right)={x}\right)\right)$
31 30 abbi2dv ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \mathrm{ran}{T}=\left\{{x}|\left({x}\in ℋ\wedge {T}\left({x}\right)={x}\right)\right\}$
32 df-rab ${⊢}\left\{{x}\in ℋ|{T}\left({x}\right)={x}\right\}=\left\{{x}|\left({x}\in ℋ\wedge {T}\left({x}\right)={x}\right)\right\}$
33 31 32 syl6eqr ${⊢}{T}\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to \mathrm{ran}{T}=\left\{{x}\in ℋ|{T}\left({x}\right)={x}\right\}$