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 ⊢ T ∈ HrmOp ∧ T ∘ T = T → ran ⁡ T ∈ C ℋ

Proof

Step Hyp Ref Expression
1 rneq ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → ran ⁡ T = ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op
2 1 eleq1d ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → ran ⁡ T ∈ C ℋ ↔ ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ C ℋ
3 eleq1 ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T ∈ HrmOp ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp
4 id ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T = if T ∈ HrmOp ∧ T ∘ T = T T I op
5 4 4 coeq12d ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T ∘ T = if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op
6 5 4 eqeq12d ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T ∘ T = T ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
7 3 6 anbi12d ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T ∈ HrmOp ∧ T ∘ T = T ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp ∧ if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
8 eleq1 ⊢ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op → I op ∈ HrmOp ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp
9 id ⊢ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op → I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
10 9 9 coeq12d ⊢ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op → I op ∘ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op
11 10 9 eqeq12d ⊢ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op → I op ∘ I op = I op ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
12 8 11 anbi12d ⊢ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op → I op ∈ HrmOp ∧ I op ∘ I op = I op ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp ∧ if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
13 idhmop ⊢ I op ∈ HrmOp
14 hoif ⊢ I op : ℋ ⟶ 1-1 onto ℋ
15 f1of ⊢ I op : ℋ ⟶ 1-1 onto ℋ → I op : ℋ ⟶ ℋ
16 14 15 ax-mp ⊢ I op : ℋ ⟶ ℋ
17 16 hoid1i ⊢ I op ∘ I op = I op
18 13 17 pm3.2i ⊢ I op ∈ HrmOp ∧ I op ∘ I op = I op
19 7 12 18 elimhyp ⊢ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp ∧ if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
20 19 simpli ⊢ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp
21 19 simpri ⊢ if T ∈ HrmOp ∧ T ∘ T = T T I op ∘ if T ∈ HrmOp ∧ T ∘ T = T T I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
22 20 21 hmopidmchi ⊢ ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ C ℋ
23 2 22 dedth ⊢ T ∈ HrmOp ∧ T ∘ T = T → ran ⁡ T ∈ C ℋ