# Metamath Proof Explorer

## Theorem hmopidmch

Description: An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of AkhiezerGlazman p. 64. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopidmch ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to \mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 eleq1d ${⊢}{T}=if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\to \left(\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}↔\mathrm{ran}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in {\mathbf{C}}_{ℋ}\right)$
3 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)$
4 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)$
5 4 4 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)$
6 5 4 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)$
7 3 6 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)$
8 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)$
9 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)$
10 9 9 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)$
11 10 9 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)$
12 8 11 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)$
13 idhmop ${⊢}{I}_{\mathrm{op}}\in \mathrm{HrmOp}$
14 hoif ${⊢}{I}_{\mathrm{op}}:ℋ\underset{1-1 onto}{⟶}ℋ$
15 f1of ${⊢}{I}_{\mathrm{op}}:ℋ\underset{1-1 onto}{⟶}ℋ\to {I}_{\mathrm{op}}:ℋ⟶ℋ$
16 14 15 ax-mp ${⊢}{I}_{\mathrm{op}}:ℋ⟶ℋ$
17 16 hoid1i ${⊢}{I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}={I}_{\mathrm{op}}$
18 13 17 pm3.2i ${⊢}\left({I}_{\mathrm{op}}\in \mathrm{HrmOp}\wedge {I}_{\mathrm{op}}\circ {I}_{\mathrm{op}}={I}_{\mathrm{op}}\right)$
19 7 12 18 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)$
20 19 simpli ${⊢}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in \mathrm{HrmOp}$
21 19 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)$
22 20 21 hmopidmchi ${⊢}\mathrm{ran}if\left(\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right),{T},{I}_{\mathrm{op}}\right)\in {\mathbf{C}}_{ℋ}$
23 2 22 dedth ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {T}\circ {T}={T}\right)\to \mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}$