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:ℋ⟶ℋ→TFnℋ
7 5 6 ax-mp ⊢TFnℋ
8 1 2 hmopidmchi ⊢ran⁡T∈Cℋ
9 8 pjfni ⊢projℎ⁡ran⁡TFnℋ
10 eqfnfv ⊢TFnℋ∧projℎ⁡ran⁡TFnℋ→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 ⊢TFnℋ∧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⋅ihT⁡y=x⋅ihT⁡y−T⁡x⋅ihT⁡y
23 18 19 21 22 syl3anc ⊢x∈ℋ∧y∈ℋ→x-ℎT⁡x⋅ihT⁡y=x⋅ihT⁡y−T⁡x⋅ihT⁡y
24 hmop ⊢T∈HrmOp∧x∈ℋ∧T⁡y∈ℋ→x⋅ihT⁡T⁡y=T⁡x⋅ihT⁡y
25 1 24 mp3an1 ⊢x∈ℋ∧T⁡y∈ℋ→x⋅ihT⁡T⁡y=T⁡x⋅ihT⁡y
26 20 25 sylan2 ⊢x∈ℋ∧y∈ℋ→x⋅ihT⁡T⁡y=T⁡x⋅ihT⁡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⋅ihT⁡T⁡y=x⋅ihT⁡y
32 26 31 eqtr3d ⊢x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡y=x⋅ihT⁡y
33 32 oveq2d ⊢x∈ℋ∧y∈ℋ→x⋅ihT⁡y−T⁡x⋅ihT⁡y=x⋅ihT⁡y−x⋅ihT⁡y
34 hicl ⊢x∈ℋ∧T⁡y∈ℋ→x⋅ihT⁡y∈ℂ
35 20 34 sylan2 ⊢x∈ℋ∧y∈ℋ→x⋅ihT⁡y∈ℂ
36 35 subidd ⊢x∈ℋ∧y∈ℋ→x⋅ihT⁡y−x⋅ihT⁡y=0
37 23 33 36 3eqtrd ⊢x∈ℋ∧y∈ℋ→x-ℎT⁡x⋅ihT⁡y=0
38 37 ralrimiva ⊢x∈ℋ→∀y∈ℋx-ℎT⁡x⋅ihT⁡y=0
39 oveq2 ⊢z=T⁡y→x-ℎT⁡x⋅ihz=x-ℎT⁡x⋅ihT⁡y
40 39 eqeq1d ⊢z=T⁡y→x-ℎT⁡x⋅ihz=0↔x-ℎT⁡x⋅ihT⁡y=0
41 40 ralrn ⊢TFnℋ→∀z∈ran⁡Tx-ℎT⁡x⋅ihz=0↔∀y∈ℋx-ℎT⁡x⋅ihT⁡y=0
42 7 41 ax-mp ⊢∀z∈ran⁡Tx-ℎT⁡x⋅ihz=0↔∀y∈ℋx-ℎT⁡x⋅ihT⁡y=0
43 38 42 sylibr ⊢x∈ℋ→∀z∈ran⁡Tx-ℎT⁡x⋅ihz=0
44 8 chssii ⊢ran⁡T⊆ℋ
45 ocel ⊢ran⁡T⊆ℋ→x-ℎT⁡x∈⊥⁡ran⁡T↔x-ℎT⁡x∈ℋ∧∀z∈ran⁡Tx-ℎT⁡x⋅ihz=0
46 44 45 ax-mp ⊢x-ℎT⁡x∈⊥⁡ran⁡T↔x-ℎT⁡x∈ℋ∧∀z∈ran⁡Tx-ℎT⁡x⋅ihz=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