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 e. HrmOp
hmopidmch.2 
|- ( T o. T ) = T
Assertion hmopidmchi 
|- ran T e. CH

Proof

Step Hyp Ref Expression
1 hmopidmch.1 
 |-  T e. HrmOp
2 hmopidmch.2 
 |-  ( T o. T ) = T
3 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
4 1 3 ax-mp 
 |-  T e. LinOp
5 4 rnelshi 
 |-  ran T e. SH
6 eqid 
 |-  ( normh o. -h ) = ( normh o. -h )
7 6 hilxmet 
 |-  ( normh o. -h ) e. ( *Met ` ~H )
8 eqid 
 |-  ( MetOpen ` ( normh o. -h ) ) = ( MetOpen ` ( normh o. -h ) )
9 8 methaus 
 |-  ( ( normh o. -h ) e. ( *Met ` ~H ) -> ( MetOpen ` ( normh o. -h ) ) e. Haus )
10 7 9 mp1i 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( MetOpen ` ( normh o. -h ) ) e. Haus )
11 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
12 11 6 hhims 
 |-  ( normh o. -h ) = ( IndMet ` <. <. +h , .h >. , normh >. )
13 11 12 8 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) )
14 resss 
 |-  ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
15 13 14 eqsstri 
 |-  ~~>v C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
16 15 ssbri 
 |-  ( f ~~>v x -> f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) x )
17 16 adantl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) x )
18 8 mopntopon 
 |-  ( ( normh o. -h ) e. ( *Met ` ~H ) -> ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) )
19 7 18 mp1i 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) )
20 4 lnopfi 
 |-  T : ~H --> ~H
21 20 a1i 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> T : ~H --> ~H )
22 21 feqmptd 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> T = ( y e. ~H |-> ( T ` y ) ) )
23 hmopbdoptHIL 
 |-  ( T e. HrmOp -> T e. BndLinOp )
24 1 23 ax-mp 
 |-  T e. BndLinOp
25 lnopcnbd 
 |-  ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) )
26 4 25 ax-mp 
 |-  ( T e. ContOp <-> T e. BndLinOp )
27 24 26 mpbir 
 |-  T e. ContOp
28 6 8 hhcno 
 |-  ContOp = ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) )
29 27 28 eleqtri 
 |-  T e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) )
30 22 29 eqeltrrdi 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( y e. ~H |-> ( T ` y ) ) e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
31 19 cnmptid 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( y e. ~H |-> y ) e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
32 11 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
33 11 hhvs 
 |-  -h = ( -v ` <. <. +h , .h >. , normh >. )
34 12 8 33 vmcn 
 |-  ( <. <. +h , .h >. , normh >. e. NrmCVec -> -h e. ( ( ( MetOpen ` ( normh o. -h ) ) tX ( MetOpen ` ( normh o. -h ) ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
35 32 34 mp1i 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> -h e. ( ( ( MetOpen ` ( normh o. -h ) ) tX ( MetOpen ` ( normh o. -h ) ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
36 19 30 31 35 cnmpt12f 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( y e. ~H |-> ( ( T ` y ) -h y ) ) e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
37 17 36 lmcn 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` x ) )
38 simpl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> f : NN --> ran T )
39 5 shssii 
 |-  ran T C_ ~H
40 fss 
 |-  ( ( f : NN --> ran T /\ ran T C_ ~H ) -> f : NN --> ~H )
41 38 39 40 sylancl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> f : NN --> ~H )
42 41 ffvelrnda 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( f ` k ) e. ~H )
43 fveq2 
 |-  ( y = ( f ` k ) -> ( T ` y ) = ( T ` ( f ` k ) ) )
44 id 
 |-  ( y = ( f ` k ) -> y = ( f ` k ) )
45 43 44 oveq12d 
 |-  ( y = ( f ` k ) -> ( ( T ` y ) -h y ) = ( ( T ` ( f ` k ) ) -h ( f ` k ) ) )
46 eqid 
 |-  ( y e. ~H |-> ( ( T ` y ) -h y ) ) = ( y e. ~H |-> ( ( T ` y ) -h y ) )
47 ovex 
 |-  ( ( T ` ( f ` k ) ) -h ( f ` k ) ) e. _V
48 45 46 47 fvmpt 
 |-  ( ( f ` k ) e. ~H -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` ( f ` k ) ) = ( ( T ` ( f ` k ) ) -h ( f ` k ) ) )
49 42 48 syl 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` ( f ` k ) ) = ( ( T ` ( f ` k ) ) -h ( f ` k ) ) )
50 ffn 
 |-  ( T : ~H --> ~H -> T Fn ~H )
51 20 50 ax-mp 
 |-  T Fn ~H
52 fveq2 
 |-  ( y = ( T ` x ) -> ( T ` y ) = ( T ` ( T ` x ) ) )
53 id 
 |-  ( y = ( T ` x ) -> y = ( T ` x ) )
54 52 53 eqeq12d 
 |-  ( y = ( T ` x ) -> ( ( T ` y ) = y <-> ( T ` ( T ` x ) ) = ( T ` x ) ) )
55 54 ralrn 
 |-  ( T Fn ~H -> ( A. y e. ran T ( T ` y ) = y <-> A. x e. ~H ( T ` ( T ` x ) ) = ( T ` x ) ) )
56 51 55 ax-mp 
 |-  ( A. y e. ran T ( T ` y ) = y <-> A. x e. ~H ( T ` ( T ` x ) ) = ( T ` x ) )
57 20 20 hocoi 
 |-  ( x e. ~H -> ( ( T o. T ) ` x ) = ( T ` ( T ` x ) ) )
58 2 fveq1i 
 |-  ( ( T o. T ) ` x ) = ( T ` x )
59 57 58 eqtr3di 
 |-  ( x e. ~H -> ( T ` ( T ` x ) ) = ( T ` x ) )
60 56 59 mprgbir 
 |-  A. y e. ran T ( T ` y ) = y
61 ffvelrn 
 |-  ( ( f : NN --> ran T /\ k e. NN ) -> ( f ` k ) e. ran T )
62 61 adantlr 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( f ` k ) e. ran T )
63 43 44 eqeq12d 
 |-  ( y = ( f ` k ) -> ( ( T ` y ) = y <-> ( T ` ( f ` k ) ) = ( f ` k ) ) )
64 63 rspccv 
 |-  ( A. y e. ran T ( T ` y ) = y -> ( ( f ` k ) e. ran T -> ( T ` ( f ` k ) ) = ( f ` k ) ) )
65 60 62 64 mpsyl 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( T ` ( f ` k ) ) = ( f ` k ) )
66 65 42 eqeltrd 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( T ` ( f ` k ) ) e. ~H )
67 hvsubeq0 
 |-  ( ( ( T ` ( f ` k ) ) e. ~H /\ ( f ` k ) e. ~H ) -> ( ( ( T ` ( f ` k ) ) -h ( f ` k ) ) = 0h <-> ( T ` ( f ` k ) ) = ( f ` k ) ) )
68 66 42 67 syl2anc 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( ( T ` ( f ` k ) ) -h ( f ` k ) ) = 0h <-> ( T ` ( f ` k ) ) = ( f ` k ) ) )
69 65 68 mpbird 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( T ` ( f ` k ) ) -h ( f ` k ) ) = 0h )
70 49 69 eqtrd 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` ( f ` k ) ) = 0h )
71 fvco3 
 |-  ( ( f : NN --> ran T /\ k e. NN ) -> ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ` k ) = ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` ( f ` k ) ) )
72 71 adantlr 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ` k ) = ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` ( f ` k ) ) )
73 ax-hv0cl 
 |-  0h e. ~H
74 73 elexi 
 |-  0h e. _V
75 74 fvconst2 
 |-  ( k e. NN -> ( ( NN X. { 0h } ) ` k ) = 0h )
76 75 adantl 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( NN X. { 0h } ) ` k ) = 0h )
77 70 72 76 3eqtr4d 
 |-  ( ( ( f : NN --> ran T /\ f ~~>v x ) /\ k e. NN ) -> ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ` k ) = ( ( NN X. { 0h } ) ` k ) )
78 77 ralrimiva 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> A. k e. NN ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ` k ) = ( ( NN X. { 0h } ) ` k ) )
79 ovex 
 |-  ( ( T ` y ) -h y ) e. _V
80 79 46 fnmpti 
 |-  ( y e. ~H |-> ( ( T ` y ) -h y ) ) Fn ~H
81 fnfco 
 |-  ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) Fn ~H /\ f : NN --> ~H ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) Fn NN )
82 80 41 81 sylancr 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) Fn NN )
83 74 fconst 
 |-  ( NN X. { 0h } ) : NN --> { 0h }
84 ffn 
 |-  ( ( NN X. { 0h } ) : NN --> { 0h } -> ( NN X. { 0h } ) Fn NN )
85 83 84 ax-mp 
 |-  ( NN X. { 0h } ) Fn NN
86 eqfnfv 
 |-  ( ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) Fn NN /\ ( NN X. { 0h } ) Fn NN ) -> ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) = ( NN X. { 0h } ) <-> A. k e. NN ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ` k ) = ( ( NN X. { 0h } ) ` k ) ) )
87 82 85 86 sylancl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) = ( NN X. { 0h } ) <-> A. k e. NN ( ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) ` k ) = ( ( NN X. { 0h } ) ` k ) ) )
88 78 87 mpbird 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) o. f ) = ( NN X. { 0h } ) )
89 vex 
 |-  x e. _V
90 89 hlimveci 
 |-  ( f ~~>v x -> x e. ~H )
91 90 adantl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> x e. ~H )
92 fveq2 
 |-  ( y = x -> ( T ` y ) = ( T ` x ) )
93 id 
 |-  ( y = x -> y = x )
94 92 93 oveq12d 
 |-  ( y = x -> ( ( T ` y ) -h y ) = ( ( T ` x ) -h x ) )
95 ovex 
 |-  ( ( T ` x ) -h x ) e. _V
96 94 46 95 fvmpt 
 |-  ( x e. ~H -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` x ) = ( ( T ` x ) -h x ) )
97 91 96 syl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( y e. ~H |-> ( ( T ` y ) -h y ) ) ` x ) = ( ( T ` x ) -h x ) )
98 37 88 97 3brtr3d 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ( T ` x ) -h x ) )
99 73 a1i 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> 0h e. ~H )
100 1zzd 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> 1 e. ZZ )
101 nnuz 
 |-  NN = ( ZZ>= ` 1 )
102 101 lmconst 
 |-  ( ( ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) /\ 0h e. ~H /\ 1 e. ZZ ) -> ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) 0h )
103 19 99 100 102 syl3anc 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( NN X. { 0h } ) ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) 0h )
104 10 98 103 lmmo 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( T ` x ) -h x ) = 0h )
105 20 ffvelrni 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
106 91 105 syl 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( T ` x ) e. ~H )
107 hvsubeq0 
 |-  ( ( ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( ( T ` x ) -h x ) = 0h <-> ( T ` x ) = x ) )
108 106 91 107 syl2anc 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( ( ( T ` x ) -h x ) = 0h <-> ( T ` x ) = x ) )
109 104 108 mpbid 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( T ` x ) = x )
110 fnfvelrn 
 |-  ( ( T Fn ~H /\ x e. ~H ) -> ( T ` x ) e. ran T )
111 51 91 110 sylancr 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> ( T ` x ) e. ran T )
112 109 111 eqeltrrd 
 |-  ( ( f : NN --> ran T /\ f ~~>v x ) -> x e. ran T )
113 112 gen2 
 |-  A. f A. x ( ( f : NN --> ran T /\ f ~~>v x ) -> x e. ran T )
114 isch2 
 |-  ( ran T e. CH <-> ( ran T e. SH /\ A. f A. x ( ( f : NN --> ran T /\ f ~~>v x ) -> x e. ran T ) ) )
115 5 113 114 mpbir2an 
 |-  ran T e. CH