# Metamath Proof Explorer

## Theorem hmopidmpji

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Halmos seems to omit the proof that H is a closed subspace, which is not trivial as hmopidmchi shows.) (Contributed by NM, 22-Apr-2006) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hmopidmch.1 $⊢ T ∈ HrmOp$
hmopidmch.2 $⊢ T ∘ T = T$
Assertion hmopidmpji $⊢ T = proj ℎ ⁡ ran ⁡ T$

### Proof

Step Hyp Ref Expression
1 hmopidmch.1 $⊢ T ∈ HrmOp$
2 hmopidmch.2 $⊢ T ∘ T = T$
3 hmoplin $⊢ T ∈ HrmOp → T ∈ LinOp$
4 1 3 ax-mp $⊢ T ∈ LinOp$
5 4 lnopfi $⊢ T : ℋ ⟶ ℋ$
6 ffn $⊢ T : ℋ ⟶ ℋ → T Fn ℋ$
7 5 6 ax-mp $⊢ T Fn ℋ$
8 1 2 hmopidmchi $⊢ ran ⁡ T ∈ C ℋ$
9 8 pjfni $⊢ proj ℎ ⁡ ran ⁡ T Fn ℋ$
10 eqfnfv $⊢ T Fn ℋ ∧ proj ℎ ⁡ ran ⁡ T Fn ℋ → T = proj ℎ ⁡ ran ⁡ T ↔ ∀ x ∈ ℋ T ⁡ x = proj ℎ ⁡ ran ⁡ T ⁡ x$
11 7 9 10 mp2an $⊢ T = proj ℎ ⁡ ran ⁡ T ↔ ∀ x ∈ ℋ T ⁡ x = proj ℎ ⁡ ran ⁡ T ⁡ x$
12 fnfvelrn $⊢ T Fn ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ran ⁡ T$
13 7 12 mpan $⊢ x ∈ ℋ → T ⁡ x ∈ ran ⁡ T$
14 id $⊢ x ∈ ℋ → x ∈ ℋ$
15 5 ffvelrni $⊢ x ∈ ℋ → T ⁡ x ∈ ℋ$
16 hvsubcl $⊢ x ∈ ℋ ∧ T ⁡ x ∈ ℋ → x - ℎ T ⁡ x ∈ ℋ$
17 14 15 16 syl2anc $⊢ x ∈ ℋ → x - ℎ T ⁡ x ∈ ℋ$
18 simpl $⊢ x ∈ ℋ ∧ y ∈ ℋ → x ∈ ℋ$
19 15 adantr $⊢ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ∈ ℋ$
20 5 ffvelrni $⊢ y ∈ ℋ → T ⁡ y ∈ ℋ$
21 20 adantl $⊢ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ$
22 his2sub $⊢ x ∈ ℋ ∧ T ⁡ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → x - ℎ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih T ⁡ y − T ⁡ x ⋅ ih T ⁡ y$
23 18 19 21 22 syl3anc $⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih T ⁡ y − T ⁡ x ⋅ ih T ⁡ y$
24 hmop $⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → x ⋅ ih T ⁡ T ⁡ y = T ⁡ x ⋅ ih T ⁡ y$
25 1 24 mp3an1 $⊢ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → x ⋅ ih T ⁡ T ⁡ y = T ⁡ x ⋅ ih T ⁡ y$
26 20 25 sylan2 $⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ T ⁡ y = T ⁡ x ⋅ ih T ⁡ y$
27 2 fveq1i $⊢ T ∘ T ⁡ y = T ⁡ y$
28 5 5 hocoi $⊢ y ∈ ℋ → T ∘ T ⁡ y = T ⁡ T ⁡ y$
29 27 28 syl5reqr $⊢ y ∈ ℋ → T ⁡ T ⁡ y = T ⁡ y$
30 29 adantl $⊢ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ T ⁡ y = T ⁡ y$
31 30 oveq2d $⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ T ⁡ y = x ⋅ ih T ⁡ y$
32 26 31 eqtr3d $⊢ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih T ⁡ y$
33 32 oveq2d $⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y − T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih T ⁡ y − x ⋅ ih T ⁡ y$
34 hicl $⊢ x ∈ ℋ ∧ T ⁡ y ∈ ℋ → x ⋅ ih T ⁡ y ∈ ℂ$
35 20 34 sylan2 $⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y ∈ ℂ$
36 35 subidd $⊢ x ∈ ℋ ∧ y ∈ ℋ → x ⋅ ih T ⁡ y − x ⋅ ih T ⁡ y = 0$
37 23 33 36 3eqtrd $⊢ x ∈ ℋ ∧ y ∈ ℋ → x - ℎ T ⁡ x ⋅ ih T ⁡ y = 0$
38 37 ralrimiva $⊢ x ∈ ℋ → ∀ y ∈ ℋ x - ℎ T ⁡ x ⋅ ih T ⁡ y = 0$
39 oveq2 $⊢ z = T ⁡ y → x - ℎ T ⁡ x ⋅ ih z = x - ℎ T ⁡ x ⋅ ih T ⁡ y$
40 39 eqeq1d $⊢ z = T ⁡ y → x - ℎ T ⁡ x ⋅ ih z = 0 ↔ x - ℎ T ⁡ x ⋅ ih T ⁡ y = 0$
41 40 ralrn $⊢ T Fn ℋ → ∀ z ∈ ran ⁡ T x - ℎ T ⁡ x ⋅ ih z = 0 ↔ ∀ y ∈ ℋ x - ℎ T ⁡ x ⋅ ih T ⁡ y = 0$
42 7 41 ax-mp $⊢ ∀ z ∈ ran ⁡ T x - ℎ T ⁡ x ⋅ ih z = 0 ↔ ∀ y ∈ ℋ x - ℎ T ⁡ x ⋅ ih T ⁡ y = 0$
43 38 42 sylibr $⊢ x ∈ ℋ → ∀ z ∈ ran ⁡ T x - ℎ T ⁡ x ⋅ ih z = 0$
44 8 chssii $⊢ ran ⁡ T ⊆ ℋ$
45 ocel $⊢ ran ⁡ T ⊆ ℋ → x - ℎ T ⁡ x ∈ ⊥ ⁡ ran ⁡ T ↔ x - ℎ T ⁡ x ∈ ℋ ∧ ∀ z ∈ ran ⁡ T x - ℎ T ⁡ x ⋅ ih z = 0$
46 44 45 ax-mp $⊢ x - ℎ T ⁡ x ∈ ⊥ ⁡ ran ⁡ T ↔ x - ℎ T ⁡ x ∈ ℋ ∧ ∀ z ∈ ran ⁡ T x - ℎ T ⁡ x ⋅ ih z = 0$
47 17 43 46 sylanbrc $⊢ x ∈ ℋ → x - ℎ T ⁡ x ∈ ⊥ ⁡ ran ⁡ T$
48 8 pjcompi $⊢ T ⁡ x ∈ ran ⁡ T ∧ x - ℎ T ⁡ x ∈ ⊥ ⁡ ran ⁡ T → proj ℎ ⁡ ran ⁡ T ⁡ T ⁡ x + ℎ x - ℎ T ⁡ x = T ⁡ x$
49 13 47 48 syl2anc $⊢ x ∈ ℋ → proj ℎ ⁡ ran ⁡ T ⁡ T ⁡ x + ℎ x - ℎ T ⁡ x = T ⁡ x$
50 hvpncan3 $⊢ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → T ⁡ x + ℎ x - ℎ T ⁡ x = x$
51 15 14 50 syl2anc $⊢ x ∈ ℋ → T ⁡ x + ℎ x - ℎ T ⁡ x = x$
52 51 fveq2d $⊢ x ∈ ℋ → proj ℎ ⁡ ran ⁡ T ⁡ T ⁡ x + ℎ x - ℎ T ⁡ x = proj ℎ ⁡ ran ⁡ T ⁡ x$
53 49 52 eqtr3d $⊢ x ∈ ℋ → T ⁡ x = proj ℎ ⁡ ran ⁡ T ⁡ x$
54 11 53 mprgbir $⊢ T = proj ℎ ⁡ ran ⁡ T$