# Metamath Proof Explorer

## Theorem hmopidmchi

Description: An idempotent Hermitian operator generates a closed subspace. Part of proof of Theorem of AkhiezerGlazman p. 64. (Contributed by NM, 21-Apr-2006) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hmopidmch.1 ${⊢}{T}\in \mathrm{HrmOp}$
hmopidmch.2 ${⊢}{T}\circ {T}={T}$
Assertion hmopidmchi ${⊢}\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 hmopidmch.1 ${⊢}{T}\in \mathrm{HrmOp}$
2 hmopidmch.2 ${⊢}{T}\circ {T}={T}$
3 hmoplin ${⊢}{T}\in \mathrm{HrmOp}\to {T}\in \mathrm{LinOp}$
4 1 3 ax-mp ${⊢}{T}\in \mathrm{LinOp}$
5 4 rnelshi ${⊢}\mathrm{ran}{T}\in {\mathbf{S}}_{ℋ}$
6 eqid ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}={norm}_{ℎ}\circ {-}_{ℎ}$
7 6 hilxmet ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}\in \mathrm{\infty Met}\left(ℋ\right)$
8 eqid ${⊢}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)=\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)$
9 8 methaus ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}\in \mathrm{\infty Met}\left(ℋ\right)\to \mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\in \mathrm{Haus}$
10 7 9 mp1i
11 eqid ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
12 11 6 hhims ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
13 11 12 8 hhlm
14 resss
15 13 14 eqsstri
16 15 ssbri
18 8 mopntopon ${⊢}{norm}_{ℎ}\circ {-}_{ℎ}\in \mathrm{\infty Met}\left(ℋ\right)\to \mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\in \mathrm{TopOn}\left(ℋ\right)$
19 7 18 mp1i
20 4 lnopfi ${⊢}{T}:ℋ⟶ℋ$
21 20 a1i
22 21 feqmptd
23 hmopbdoptHIL ${⊢}{T}\in \mathrm{HrmOp}\to {T}\in \mathrm{BndLinOp}$
24 1 23 ax-mp ${⊢}{T}\in \mathrm{BndLinOp}$
25 lnopcnbd ${⊢}{T}\in \mathrm{LinOp}\to \left({T}\in \mathrm{ContOp}↔{T}\in \mathrm{BndLinOp}\right)$
26 4 25 ax-mp ${⊢}{T}\in \mathrm{ContOp}↔{T}\in \mathrm{BndLinOp}$
27 24 26 mpbir ${⊢}{T}\in \mathrm{ContOp}$
28 6 8 hhcno ${⊢}\mathrm{ContOp}=\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\mathrm{Cn}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)$
29 27 28 eleqtri ${⊢}{T}\in \left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\mathrm{Cn}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)$
30 22 29 eqeltrrdi
31 19 cnmptid
32 11 hhnv ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$
33 11 hhvs ${⊢}{-}_{ℎ}={-}_{v}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
34 12 8 33 vmcn ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\to {-}_{ℎ}\in \left(\left(\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right){×}_{t}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)\mathrm{Cn}\mathrm{MetOpen}\left({norm}_{ℎ}\circ {-}_{ℎ}\right)\right)$
35 32 34 mp1i
36 19 30 31 35 cnmpt12f
37 17 36 lmcn
38 simpl
39 5 shssii ${⊢}\mathrm{ran}{T}\subseteq ℋ$
40 fss ${⊢}\left({f}:ℕ⟶\mathrm{ran}{T}\wedge \mathrm{ran}{T}\subseteq ℋ\right)\to {f}:ℕ⟶ℋ$
41 38 39 40 sylancl
42 41 ffvelrnda
43 fveq2 ${⊢}{y}={f}\left({k}\right)\to {T}\left({y}\right)={T}\left({f}\left({k}\right)\right)$
44 id ${⊢}{y}={f}\left({k}\right)\to {y}={f}\left({k}\right)$
45 43 44 oveq12d ${⊢}{y}={f}\left({k}\right)\to {T}\left({y}\right){-}_{ℎ}{y}={T}\left({f}\left({k}\right)\right){-}_{ℎ}{f}\left({k}\right)$
46 eqid ${⊢}\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)=\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)$
47 ovex ${⊢}{T}\left({f}\left({k}\right)\right){-}_{ℎ}{f}\left({k}\right)\in \mathrm{V}$
48 45 46 47 fvmpt ${⊢}{f}\left({k}\right)\in ℋ\to \left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\left({f}\left({k}\right)\right)={T}\left({f}\left({k}\right)\right){-}_{ℎ}{f}\left({k}\right)$
49 42 48 syl
50 ffn ${⊢}{T}:ℋ⟶ℋ\to {T}Fnℋ$
51 20 50 ax-mp ${⊢}{T}Fnℋ$
52 fveq2 ${⊢}{y}={T}\left({x}\right)\to {T}\left({y}\right)={T}\left({T}\left({x}\right)\right)$
53 id ${⊢}{y}={T}\left({x}\right)\to {y}={T}\left({x}\right)$
54 52 53 eqeq12d ${⊢}{y}={T}\left({x}\right)\to \left({T}\left({y}\right)={y}↔{T}\left({T}\left({x}\right)\right)={T}\left({x}\right)\right)$
55 54 ralrn ${⊢}{T}Fnℋ\to \left(\forall {y}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({T}\left({x}\right)\right)={T}\left({x}\right)\right)$
56 51 55 ax-mp ${⊢}\forall {y}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({T}\left({x}\right)\right)={T}\left({x}\right)$
57 2 fveq1i ${⊢}\left({T}\circ {T}\right)\left({x}\right)={T}\left({x}\right)$
58 20 20 hocoi ${⊢}{x}\in ℋ\to \left({T}\circ {T}\right)\left({x}\right)={T}\left({T}\left({x}\right)\right)$
59 57 58 syl5reqr ${⊢}{x}\in ℋ\to {T}\left({T}\left({x}\right)\right)={T}\left({x}\right)$
60 56 59 mprgbir ${⊢}\forall {y}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={y}$
61 ffvelrn ${⊢}\left({f}:ℕ⟶\mathrm{ran}{T}\wedge {k}\in ℕ\right)\to {f}\left({k}\right)\in \mathrm{ran}{T}$
63 43 44 eqeq12d ${⊢}{y}={f}\left({k}\right)\to \left({T}\left({y}\right)={y}↔{T}\left({f}\left({k}\right)\right)={f}\left({k}\right)\right)$
64 63 rspccv ${⊢}\forall {y}\in \mathrm{ran}{T}\phantom{\rule{.4em}{0ex}}{T}\left({y}\right)={y}\to \left({f}\left({k}\right)\in \mathrm{ran}{T}\to {T}\left({f}\left({k}\right)\right)={f}\left({k}\right)\right)$
65 60 62 64 mpsyl
66 65 42 eqeltrd
67 hvsubeq0 ${⊢}\left({T}\left({f}\left({k}\right)\right)\in ℋ\wedge {f}\left({k}\right)\in ℋ\right)\to \left({T}\left({f}\left({k}\right)\right){-}_{ℎ}{f}\left({k}\right)={0}_{ℎ}↔{T}\left({f}\left({k}\right)\right)={f}\left({k}\right)\right)$
68 66 42 67 syl2anc
69 65 68 mpbird
70 49 69 eqtrd
71 fvco3 ${⊢}\left({f}:ℕ⟶\mathrm{ran}{T}\wedge {k}\in ℕ\right)\to \left(\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\circ {f}\right)\left({k}\right)=\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\left({f}\left({k}\right)\right)$
73 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
74 73 elexi ${⊢}{0}_{ℎ}\in \mathrm{V}$
75 74 fvconst2 ${⊢}{k}\in ℕ\to \left(ℕ×\left\{{0}_{ℎ}\right\}\right)\left({k}\right)={0}_{ℎ}$
77 70 72 76 3eqtr4d
78 77 ralrimiva
79 ovex ${⊢}{T}\left({y}\right){-}_{ℎ}{y}\in \mathrm{V}$
80 79 46 fnmpti ${⊢}\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)Fnℋ$
81 fnfco ${⊢}\left(\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)Fnℋ\wedge {f}:ℕ⟶ℋ\right)\to \left(\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\circ {f}\right)Fnℕ$
82 80 41 81 sylancr
83 74 fconst ${⊢}\left(ℕ×\left\{{0}_{ℎ}\right\}\right):ℕ⟶\left\{{0}_{ℎ}\right\}$
84 ffn ${⊢}\left(ℕ×\left\{{0}_{ℎ}\right\}\right):ℕ⟶\left\{{0}_{ℎ}\right\}\to \left(ℕ×\left\{{0}_{ℎ}\right\}\right)Fnℕ$
85 83 84 ax-mp ${⊢}\left(ℕ×\left\{{0}_{ℎ}\right\}\right)Fnℕ$
86 eqfnfv ${⊢}\left(\left(\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\circ {f}\right)Fnℕ\wedge \left(ℕ×\left\{{0}_{ℎ}\right\}\right)Fnℕ\right)\to \left(\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\circ {f}=ℕ×\left\{{0}_{ℎ}\right\}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\circ {f}\right)\left({k}\right)=\left(ℕ×\left\{{0}_{ℎ}\right\}\right)\left({k}\right)\right)$
87 82 85 86 sylancl
88 78 87 mpbird
89 vex ${⊢}{x}\in \mathrm{V}$
90 89 hlimveci
92 fveq2 ${⊢}{y}={x}\to {T}\left({y}\right)={T}\left({x}\right)$
93 id ${⊢}{y}={x}\to {y}={x}$
94 92 93 oveq12d ${⊢}{y}={x}\to {T}\left({y}\right){-}_{ℎ}{y}={T}\left({x}\right){-}_{ℎ}{x}$
95 ovex ${⊢}{T}\left({x}\right){-}_{ℎ}{x}\in \mathrm{V}$
96 94 46 95 fvmpt ${⊢}{x}\in ℋ\to \left({y}\in ℋ⟼{T}\left({y}\right){-}_{ℎ}{y}\right)\left({x}\right)={T}\left({x}\right){-}_{ℎ}{x}$
97 91 96 syl
98 37 88 97 3brtr3d
99 73 a1i
100 1zzd
101 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
102 101 lmconst
103 19 99 100 102 syl3anc
104 10 98 103 lmmo
105 20 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
106 91 105 syl
107 hvsubeq0 ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {x}\in ℋ\right)\to \left({T}\left({x}\right){-}_{ℎ}{x}={0}_{ℎ}↔{T}\left({x}\right)={x}\right)$
108 106 91 107 syl2anc
109 104 108 mpbid
110 fnfvelrn ${⊢}\left({T}Fnℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in \mathrm{ran}{T}$
111 51 91 110 sylancr
112 109 111 eqeltrrd
113 112 gen2
114 isch2
115 5 113 114 mpbir2an ${⊢}\mathrm{ran}{T}\in {\mathbf{C}}_{ℋ}$