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 |
2
|
fveq1i |
|- ( ( T o. T ) ` x ) = ( T ` x ) |
58 |
20 20
|
hocoi |
|- ( x e. ~H -> ( ( T o. T ) ` x ) = ( T ` ( T ` x ) ) ) |
59 |
57 58
|
syl5reqr |
|- ( 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 |