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 ffvelcdmi ⊢ 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 ffvelcdmi ⊢ 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 5 5 hocoi ⊢ y ∈ ℋ → T ∘ T ⁡ y = T ⁡ T ⁡ y
28 2 fveq1i ⊢ T ∘ T ⁡ y = T ⁡ y
29 27 28 eqtr3di ⊢ 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