Metamath Proof Explorer

Theorem occllem

Description: Lemma for occl . (Contributed by NM, 7-Aug-2000) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses occl.1 
|- ( ph -> A C_ ~H )
occl.2 
|- ( ph -> F e. Cauchy )
occl.3 
|- ( ph -> F : NN --> ( _|_ ` A ) )
occl.4 
|- ( ph -> B e. A )
Assertion occllem 
|- ( ph -> ( ( ~~>v ` F ) .ih B ) = 0 )

Proof

Step Hyp Ref Expression
1 occl.1 
 |-  ( ph -> A C_ ~H )
2 occl.2 
 |-  ( ph -> F e. Cauchy )
3 occl.3 
 |-  ( ph -> F : NN --> ( _|_ ` A ) )
4 occl.4 
 |-  ( ph -> B e. A )
5 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
6 5 cnfldhaus 
 |-  ( TopOpen ` CCfld ) e. Haus
7 6 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Haus )
8 ax-hcompl 
 |-  ( F e. Cauchy -> E. x e. ~H F ~~>v x )
9 hlimf 
 |-  ~~>v : dom ~~>v --> ~H
10 ffn 
 |-  ( ~~>v : dom ~~>v --> ~H -> ~~>v Fn dom ~~>v )
11 9 10 ax-mp 
 |-  ~~>v Fn dom ~~>v
12 fnbr 
 |-  ( ( ~~>v Fn dom ~~>v /\ F ~~>v x ) -> F e. dom ~~>v )
13 11 12 mpan 
 |-  ( F ~~>v x -> F e. dom ~~>v )
14 13 rexlimivw 
 |-  ( E. x e. ~H F ~~>v x -> F e. dom ~~>v )
15 2 8 14 3syl 
 |-  ( ph -> F e. dom ~~>v )
16 ffun 
 |-  ( ~~>v : dom ~~>v --> ~H -> Fun ~~>v )
17 funfvbrb 
 |-  ( Fun ~~>v -> ( F e. dom ~~>v <-> F ~~>v ( ~~>v ` F ) ) )
18 9 16 17 mp2b 
 |-  ( F e. dom ~~>v <-> F ~~>v ( ~~>v ` F ) )
19 15 18 sylib 
 |-  ( ph -> F ~~>v ( ~~>v ` F ) )
20 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
21 eqid 
 |-  ( normh o. -h ) = ( normh o. -h )
22 20 21 hhims 
 |-  ( normh o. -h ) = ( IndMet ` <. <. +h , .h >. , normh >. )
23 eqid 
 |-  ( MetOpen ` ( normh o. -h ) ) = ( MetOpen ` ( normh o. -h ) )
24 20 22 23 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) )
25 resss 
 |-  ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
26 24 25 eqsstri 
 |-  ~~>v C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
27 26 ssbri 
 |-  ( F ~~>v ( ~~>v ` F ) -> F ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ~~>v ` F ) )
28 19 27 syl 
 |-  ( ph -> F ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ~~>v ` F ) )
29 21 hilxmet 
 |-  ( normh o. -h ) e. ( *Met ` ~H )
30 23 mopntopon 
 |-  ( ( normh o. -h ) e. ( *Met ` ~H ) -> ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) )
31 29 30 mp1i 
 |-  ( ph -> ( MetOpen ` ( normh o. -h ) ) e. ( TopOn ` ~H ) )
32 31 cnmptid 
 |-  ( ph -> ( x e. ~H |-> x ) e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
33 1 4 sseldd 
 |-  ( ph -> B e. ~H )
34 31 31 33 cnmptc 
 |-  ( ph -> ( x e. ~H |-> B ) e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( MetOpen ` ( normh o. -h ) ) ) )
35 20 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
36 20 hhip 
 |-  .ih = ( .iOLD ` <. <. +h , .h >. , normh >. )
37 36 22 23 5 dipcn 
 |-  ( <. <. +h , .h >. , normh >. e. NrmCVec -> .ih e. ( ( ( MetOpen ` ( normh o. -h ) ) tX ( MetOpen ` ( normh o. -h ) ) ) Cn ( TopOpen ` CCfld ) ) )
38 35 37 mp1i 
 |-  ( ph -> .ih e. ( ( ( MetOpen ` ( normh o. -h ) ) tX ( MetOpen ` ( normh o. -h ) ) ) Cn ( TopOpen ` CCfld ) ) )
39 31 32 34 38 cnmpt12f 
 |-  ( ph -> ( x e. ~H |-> ( x .ih B ) ) e. ( ( MetOpen ` ( normh o. -h ) ) Cn ( TopOpen ` CCfld ) ) )
40 28 39 lmcn 
 |-  ( ph -> ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ( ~~>t ` ( TopOpen ` CCfld ) ) ( ( x e. ~H |-> ( x .ih B ) ) ` ( ~~>v ` F ) ) )
41 3 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( _|_ ` A ) )
42 ocel 
 |-  ( A C_ ~H -> ( ( F ` k ) e. ( _|_ ` A ) <-> ( ( F ` k ) e. ~H /\ A. x e. A ( ( F ` k ) .ih x ) = 0 ) ) )
43 1 42 syl 
 |-  ( ph -> ( ( F ` k ) e. ( _|_ ` A ) <-> ( ( F ` k ) e. ~H /\ A. x e. A ( ( F ` k ) .ih x ) = 0 ) ) )
44 43 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) e. ( _|_ ` A ) <-> ( ( F ` k ) e. ~H /\ A. x e. A ( ( F ` k ) .ih x ) = 0 ) ) )
45 41 44 mpbid 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) e. ~H /\ A. x e. A ( ( F ` k ) .ih x ) = 0 ) )
46 45 simpld 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. ~H )
47 oveq1 
 |-  ( x = ( F ` k ) -> ( x .ih B ) = ( ( F ` k ) .ih B ) )
48 eqid 
 |-  ( x e. ~H |-> ( x .ih B ) ) = ( x e. ~H |-> ( x .ih B ) )
49 ovex 
 |-  ( ( F ` k ) .ih B ) e. _V
50 47 48 49 fvmpt 
 |-  ( ( F ` k ) e. ~H -> ( ( x e. ~H |-> ( x .ih B ) ) ` ( F ` k ) ) = ( ( F ` k ) .ih B ) )
51 46 50 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( x e. ~H |-> ( x .ih B ) ) ` ( F ` k ) ) = ( ( F ` k ) .ih B ) )
52 oveq2 
 |-  ( x = B -> ( ( F ` k ) .ih x ) = ( ( F ` k ) .ih B ) )
53 52 eqeq1d 
 |-  ( x = B -> ( ( ( F ` k ) .ih x ) = 0 <-> ( ( F ` k ) .ih B ) = 0 ) )
54 45 simprd 
 |-  ( ( ph /\ k e. NN ) -> A. x e. A ( ( F ` k ) .ih x ) = 0 )
55 4 adantr 
 |-  ( ( ph /\ k e. NN ) -> B e. A )
56 53 54 55 rspcdva 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) .ih B ) = 0 )
57 51 56 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( x e. ~H |-> ( x .ih B ) ) ` ( F ` k ) ) = 0 )
58 ocss 
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
59 1 58 syl 
 |-  ( ph -> ( _|_ ` A ) C_ ~H )
60 3 59 fssd 
 |-  ( ph -> F : NN --> ~H )
61 fvco3 
 |-  ( ( F : NN --> ~H /\ k e. NN ) -> ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ` k ) = ( ( x e. ~H |-> ( x .ih B ) ) ` ( F ` k ) ) )
62 60 61 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ` k ) = ( ( x e. ~H |-> ( x .ih B ) ) ` ( F ` k ) ) )
63 c0ex 
 |-  0 e. _V
64 63 fvconst2 
 |-  ( k e. NN -> ( ( NN X. { 0 } ) ` k ) = 0 )
65 64 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( NN X. { 0 } ) ` k ) = 0 )
66 57 62 65 3eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ` k ) = ( ( NN X. { 0 } ) ` k ) )
67 66 ralrimiva 
 |-  ( ph -> A. k e. NN ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ` k ) = ( ( NN X. { 0 } ) ` k ) )
68 ovex 
 |-  ( x .ih B ) e. _V
69 68 48 fnmpti 
 |-  ( x e. ~H |-> ( x .ih B ) ) Fn ~H
70 fnfco 
 |-  ( ( ( x e. ~H |-> ( x .ih B ) ) Fn ~H /\ F : NN --> ~H ) -> ( ( x e. ~H |-> ( x .ih B ) ) o. F ) Fn NN )
71 69 60 70 sylancr 
 |-  ( ph -> ( ( x e. ~H |-> ( x .ih B ) ) o. F ) Fn NN )
72 63 fconst 
 |-  ( NN X. { 0 } ) : NN --> { 0 }
73 ffn 
 |-  ( ( NN X. { 0 } ) : NN --> { 0 } -> ( NN X. { 0 } ) Fn NN )
74 72 73 ax-mp 
 |-  ( NN X. { 0 } ) Fn NN
75 eqfnfv 
 |-  ( ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) Fn NN /\ ( NN X. { 0 } ) Fn NN ) -> ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) = ( NN X. { 0 } ) <-> A. k e. NN ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ` k ) = ( ( NN X. { 0 } ) ` k ) ) )
76 71 74 75 sylancl 
 |-  ( ph -> ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) = ( NN X. { 0 } ) <-> A. k e. NN ( ( ( x e. ~H |-> ( x .ih B ) ) o. F ) ` k ) = ( ( NN X. { 0 } ) ` k ) ) )
77 67 76 mpbird 
 |-  ( ph -> ( ( x e. ~H |-> ( x .ih B ) ) o. F ) = ( NN X. { 0 } ) )
78 fvex 
 |-  ( ~~>v ` F ) e. _V
79 78 hlimveci 
 |-  ( F ~~>v ( ~~>v ` F ) -> ( ~~>v ` F ) e. ~H )
80 oveq1 
 |-  ( x = ( ~~>v ` F ) -> ( x .ih B ) = ( ( ~~>v ` F ) .ih B ) )
81 ovex 
 |-  ( ( ~~>v ` F ) .ih B ) e. _V
82 80 48 81 fvmpt 
 |-  ( ( ~~>v ` F ) e. ~H -> ( ( x e. ~H |-> ( x .ih B ) ) ` ( ~~>v ` F ) ) = ( ( ~~>v ` F ) .ih B ) )
83 19 79 82 3syl 
 |-  ( ph -> ( ( x e. ~H |-> ( x .ih B ) ) ` ( ~~>v ` F ) ) = ( ( ~~>v ` F ) .ih B ) )
84 40 77 83 3brtr3d 
 |-  ( ph -> ( NN X. { 0 } ) ( ~~>t ` ( TopOpen ` CCfld ) ) ( ( ~~>v ` F ) .ih B ) )
85 5 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
86 85 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
87 0cnd 
 |-  ( ph -> 0 e. CC )
88 1zzd 
 |-  ( ph -> 1 e. ZZ )
89 nnuz 
 |-  NN = ( ZZ>= ` 1 )
90 89 lmconst 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ 0 e. CC /\ 1 e. ZZ ) -> ( NN X. { 0 } ) ( ~~>t ` ( TopOpen ` CCfld ) ) 0 )
91 86 87 88 90 syl3anc 
 |-  ( ph -> ( NN X. { 0 } ) ( ~~>t ` ( TopOpen ` CCfld ) ) 0 )
92 7 84 91 lmmo 
 |-  ( ph -> ( ( ~~>v ` F ) .ih B ) = 0 )