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

Proof

Step Hyp Ref Expression
1 id ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T = if T ∈ HrmOp ∧ T ∘ T = T T I op
2 rneq ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → ran ⁡ T = ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op
3 2 fveq2d ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → proj ℎ ⁡ ran ⁡ T = proj ℎ ⁡ ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op
4 1 3 eqeq12d ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T = proj ℎ ⁡ ran ⁡ T ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op = proj ℎ ⁡ ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op
5 eleq1 ⊢ T = if T ∈ HrmOp ∧ T ∘ T = T T I op → T ∈ HrmOp ↔ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp
6 1 1 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
7 6 1 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
8 5 7 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
9 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
10 id ⊢ I op = if T ∈ HrmOp ∧ T ∘ T = T T I op → I op = if T ∈ HrmOp ∧ T ∘ T = T T I op
11 10 10 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
12 11 10 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
13 9 12 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
14 idhmop ⊢ I op ∈ HrmOp
15 hoif ⊢ I op : ℋ ⟶ 1-1 onto ℋ
16 f1of ⊢ I op : ℋ ⟶ 1-1 onto ℋ → I op : ℋ ⟶ ℋ
17 15 16 ax-mp ⊢ I op : ℋ ⟶ ℋ
18 17 hoid1i ⊢ I op ∘ I op = I op
19 14 18 pm3.2i ⊢ I op ∈ HrmOp ∧ I op ∘ I op = I op
20 8 13 19 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
21 20 simpli ⊢ if T ∈ HrmOp ∧ T ∘ T = T T I op ∈ HrmOp
22 20 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
23 21 22 hmopidmpji ⊢ if T ∈ HrmOp ∧ T ∘ T = T T I op = proj ℎ ⁡ ran ⁡ if T ∈ HrmOp ∧ T ∘ T = T T I op
24 4 23 dedth ⊢ T ∈ HrmOp ∧ T ∘ T = T → T = proj ℎ ⁡ ran ⁡ T