# 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 ffvelrnda
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`