# Metamath Proof Explorer

## Theorem hmopidmpj

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopidmpj ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to {T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to {T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)$
2 rneq ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \mathrm{ran}{T}=\mathrm{ran}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)$
3 2 fveq2d ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)$
4 1 3 eqeq12d ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left({T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)↔if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)\right)$
5 eleq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left({T}\in \mathrm{HrmOp}↔if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}\right)$
6 1 1 coeq12d ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to {T}\circ {T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)$
7 6 1 eqeq12d ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left({T}\circ {T}={T}↔if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)$
8 5 7 anbi12d ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)↔\left(if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}\wedge if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)\right)$
9 eleq1 ${⊢}{I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left({I}_{\mathrm{op}}\in \mathrm{HrmOp}↔if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}\right)$
10 id ${⊢}{I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to {I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)$
11 10 10 coeq12d ${⊢}{I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to {I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)$
12 11 10 eqeq12d ${⊢}{I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left({I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}={I}_{\mathrm{op}}↔if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)$
13 9 12 anbi12d ${⊢}{I}_{\mathrm{op}}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left(\left({I}_{\mathrm{op}}\in \mathrm{HrmOp}\wedge {I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}={I}_{\mathrm{op}}\right)↔\left(if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}\wedge if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)\right)$
14 idhmop ${⊢}{I}_{\mathrm{op}}\in \mathrm{HrmOp}$
15 hoif ${⊢}{I}_{\mathrm{op}}:ℋ\underset{1-1 onto}{⟶}ℋ$
16 f1of ${⊢}{I}_{\mathrm{op}}:ℋ\underset{1-1 onto}{⟶}ℋ\to {I}_{\mathrm{op}}:ℋ⟶ℋ$
17 15 16 ax-mp ${⊢}{I}_{\mathrm{op}}:ℋ⟶ℋ$
18 17 hoid1i ${⊢}{I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}={I}_{\mathrm{op}}$
19 14 18 pm3.2i ${⊢}\left({I}_{\mathrm{op}}\in \mathrm{HrmOp}\wedge {I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}={I}_{\mathrm{op}}\right)$
20 8 13 19 elimhyp ${⊢}\left(if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}\wedge if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)$
21 20 simpli ${⊢}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}$
22 20 simpri ${⊢}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\circ if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)$
23 21 22 hmopidmpji ${⊢}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\right)$
24 4 23 dedth ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to {T}={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}{T}\right)$