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 ( 𝜑𝐴 ⊆ ℋ )
occl.2 ( 𝜑𝐹 ∈ Cauchy )
occl.3 ( 𝜑𝐹 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) )
occl.4 ( 𝜑𝐵𝐴 )
Assertion occllem ( 𝜑 → ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) = 0 )

Proof

Step Hyp Ref Expression
1 occl.1 ( 𝜑𝐴 ⊆ ℋ )
2 occl.2 ( 𝜑𝐹 ∈ Cauchy )
3 occl.3 ( 𝜑𝐹 : ℕ ⟶ ( ⊥ ‘ 𝐴 ) )
4 occl.4 ( 𝜑𝐵𝐴 )
5 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
6 5 cnfldhaus ( TopOpen ‘ ℂfld ) ∈ Haus
7 6 a1i ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Haus )
8 ax-hcompl ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹𝑣 𝑥 )
9 hlimf 𝑣 : dom ⇝𝑣 ⟶ ℋ
10 ffn ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → ⇝𝑣 Fn dom ⇝𝑣 )
11 9 10 ax-mp 𝑣 Fn dom ⇝𝑣
12 fnbr ( ( ⇝𝑣 Fn dom ⇝𝑣𝐹𝑣 𝑥 ) → 𝐹 ∈ dom ⇝𝑣 )
13 11 12 mpan ( 𝐹𝑣 𝑥𝐹 ∈ dom ⇝𝑣 )
14 13 rexlimivw ( ∃ 𝑥 ∈ ℋ 𝐹𝑣 𝑥𝐹 ∈ dom ⇝𝑣 )
15 2 8 14 3syl ( 𝜑𝐹 ∈ dom ⇝𝑣 )
16 ffun ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → Fun ⇝𝑣 )
17 funfvbrb ( Fun ⇝𝑣 → ( 𝐹 ∈ dom ⇝𝑣𝐹𝑣 ( ⇝𝑣𝐹 ) ) )
18 9 16 17 mp2b ( 𝐹 ∈ dom ⇝𝑣𝐹𝑣 ( ⇝𝑣𝐹 ) )
19 15 18 sylib ( 𝜑𝐹𝑣 ( ⇝𝑣𝐹 ) )
20 eqid ⟨ ⟨ + , · ⟩ , norm ⟩ = ⟨ ⟨ + , · ⟩ , norm
21 eqid ( norm ∘ − ) = ( norm ∘ − )
22 20 21 hhims ( norm ∘ − ) = ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
23 eqid ( MetOpen ‘ ( norm ∘ − ) ) = ( MetOpen ‘ ( norm ∘ − ) )
24 20 22 23 hhlm 𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ↾ ( ℋ ↑m ℕ ) )
25 resss ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ↾ ( ℋ ↑m ℕ ) ) ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) )
26 24 25 eqsstri 𝑣 ⊆ ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) )
27 26 ssbri ( 𝐹𝑣 ( ⇝𝑣𝐹 ) → 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ( ⇝𝑣𝐹 ) )
28 19 27 syl ( 𝜑𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( norm ∘ − ) ) ) ( ⇝𝑣𝐹 ) )
29 21 hilxmet ( norm ∘ − ) ∈ ( ∞Met ‘ ℋ )
30 23 mopntopon ( ( norm ∘ − ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( norm ∘ − ) ) ∈ ( TopOn ‘ ℋ ) )
31 29 30 mp1i ( 𝜑 → ( MetOpen ‘ ( norm ∘ − ) ) ∈ ( TopOn ‘ ℋ ) )
32 31 cnmptid ( 𝜑 → ( 𝑥 ∈ ℋ ↦ 𝑥 ) ∈ ( ( MetOpen ‘ ( norm ∘ − ) ) Cn ( MetOpen ‘ ( norm ∘ − ) ) ) )
33 1 4 sseldd ( 𝜑𝐵 ∈ ℋ )
34 31 31 33 cnmptc ( 𝜑 → ( 𝑥 ∈ ℋ ↦ 𝐵 ) ∈ ( ( MetOpen ‘ ( norm ∘ − ) ) Cn ( MetOpen ‘ ( norm ∘ − ) ) ) )
35 20 hhnv ⟨ ⟨ + , · ⟩ , norm ⟩ ∈ NrmCVec
36 20 hhip ·ih = ( ·𝑖OLD ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
37 36 22 23 5 dipcn ( ⟨ ⟨ + , · ⟩ , norm ⟩ ∈ NrmCVec → ·ih ∈ ( ( ( MetOpen ‘ ( norm ∘ − ) ) ×t ( MetOpen ‘ ( norm ∘ − ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
38 35 37 mp1i ( 𝜑·ih ∈ ( ( ( MetOpen ‘ ( norm ∘ − ) ) ×t ( MetOpen ‘ ( norm ∘ − ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
39 31 32 34 38 cnmpt12f ( 𝜑 → ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∈ ( ( MetOpen ‘ ( norm ∘ − ) ) Cn ( TopOpen ‘ ℂfld ) ) )
40 28 39 lmcn ( 𝜑 → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( ⇝𝑣𝐹 ) ) )
41 3 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ ( ⊥ ‘ 𝐴 ) )
42 ocel ( 𝐴 ⊆ ℋ → ( ( 𝐹𝑘 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝐹𝑘 ) ∈ ℋ ∧ ∀ 𝑥𝐴 ( ( 𝐹𝑘 ) ·ih 𝑥 ) = 0 ) ) )
43 1 42 syl ( 𝜑 → ( ( 𝐹𝑘 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝐹𝑘 ) ∈ ℋ ∧ ∀ 𝑥𝐴 ( ( 𝐹𝑘 ) ·ih 𝑥 ) = 0 ) ) )
44 43 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝐹𝑘 ) ∈ ℋ ∧ ∀ 𝑥𝐴 ( ( 𝐹𝑘 ) ·ih 𝑥 ) = 0 ) ) )
45 41 44 mpbid ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) ∈ ℋ ∧ ∀ 𝑥𝐴 ( ( 𝐹𝑘 ) ·ih 𝑥 ) = 0 ) )
46 45 simpld ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ ℋ )
47 oveq1 ( 𝑥 = ( 𝐹𝑘 ) → ( 𝑥 ·ih 𝐵 ) = ( ( 𝐹𝑘 ) ·ih 𝐵 ) )
48 eqid ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) )
49 ovex ( ( 𝐹𝑘 ) ·ih 𝐵 ) ∈ V
50 47 48 49 fvmpt ( ( 𝐹𝑘 ) ∈ ℋ → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( 𝐹𝑘 ) ) = ( ( 𝐹𝑘 ) ·ih 𝐵 ) )
51 46 50 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( 𝐹𝑘 ) ) = ( ( 𝐹𝑘 ) ·ih 𝐵 ) )
52 oveq2 ( 𝑥 = 𝐵 → ( ( 𝐹𝑘 ) ·ih 𝑥 ) = ( ( 𝐹𝑘 ) ·ih 𝐵 ) )
53 52 eqeq1d ( 𝑥 = 𝐵 → ( ( ( 𝐹𝑘 ) ·ih 𝑥 ) = 0 ↔ ( ( 𝐹𝑘 ) ·ih 𝐵 ) = 0 ) )
54 45 simprd ( ( 𝜑𝑘 ∈ ℕ ) → ∀ 𝑥𝐴 ( ( 𝐹𝑘 ) ·ih 𝑥 ) = 0 )
55 4 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐵𝐴 )
56 53 54 55 rspcdva ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) ·ih 𝐵 ) = 0 )
57 51 56 eqtrd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( 𝐹𝑘 ) ) = 0 )
58 ocss ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
59 1 58 syl ( 𝜑 → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
60 3 59 fssd ( 𝜑𝐹 : ℕ ⟶ ℋ )
61 fvco3 ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( 𝐹𝑘 ) ) )
62 60 61 sylan ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( 𝐹𝑘 ) ) )
63 c0ex 0 ∈ V
64 63 fvconst2 ( 𝑘 ∈ ℕ → ( ( ℕ × { 0 } ) ‘ 𝑘 ) = 0 )
65 64 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ℕ × { 0 } ) ‘ 𝑘 ) = 0 )
66 57 62 65 3eqtr4d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( ℕ × { 0 } ) ‘ 𝑘 ) )
67 66 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( ℕ × { 0 } ) ‘ 𝑘 ) )
68 ovex ( 𝑥 ·ih 𝐵 ) ∈ V
69 68 48 fnmpti ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) Fn ℋ
70 fnfco ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) Fn ℋ ∧ 𝐹 : ℕ ⟶ ℋ ) → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) Fn ℕ )
71 69 60 70 sylancr ( 𝜑 → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) Fn ℕ )
72 63 fconst ( ℕ × { 0 } ) : ℕ ⟶ { 0 }
73 ffn ( ( ℕ × { 0 } ) : ℕ ⟶ { 0 } → ( ℕ × { 0 } ) Fn ℕ )
74 72 73 ax-mp ( ℕ × { 0 } ) Fn ℕ
75 eqfnfv ( ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) Fn ℕ ∧ ( ℕ × { 0 } ) Fn ℕ ) → ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) = ( ℕ × { 0 } ) ↔ ∀ 𝑘 ∈ ℕ ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( ℕ × { 0 } ) ‘ 𝑘 ) ) )
76 71 74 75 sylancl ( 𝜑 → ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) = ( ℕ × { 0 } ) ↔ ∀ 𝑘 ∈ ℕ ( ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) ‘ 𝑘 ) = ( ( ℕ × { 0 } ) ‘ 𝑘 ) ) )
77 67 76 mpbird ( 𝜑 → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ∘ 𝐹 ) = ( ℕ × { 0 } ) )
78 fvex ( ⇝𝑣𝐹 ) ∈ V
79 78 hlimveci ( 𝐹𝑣 ( ⇝𝑣𝐹 ) → ( ⇝𝑣𝐹 ) ∈ ℋ )
80 oveq1 ( 𝑥 = ( ⇝𝑣𝐹 ) → ( 𝑥 ·ih 𝐵 ) = ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) )
81 ovex ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) ∈ V
82 80 48 81 fvmpt ( ( ⇝𝑣𝐹 ) ∈ ℋ → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( ⇝𝑣𝐹 ) ) = ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) )
83 19 79 82 3syl ( 𝜑 → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐵 ) ) ‘ ( ⇝𝑣𝐹 ) ) = ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) )
84 40 77 83 3brtr3d ( 𝜑 → ( ℕ × { 0 } ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) )
85 5 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
86 85 a1i ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
87 0cnd ( 𝜑 → 0 ∈ ℂ )
88 1zzd ( 𝜑 → 1 ∈ ℤ )
89 nnuz ℕ = ( ℤ ‘ 1 )
90 89 lmconst ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { 0 } ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 0 )
91 86 87 88 90 syl3anc ( 𝜑 → ( ℕ × { 0 } ) ( ⇝𝑡 ‘ ( TopOpen ‘ ℂfld ) ) 0 )
92 7 84 91 lmmo ( 𝜑 → ( ( ⇝𝑣𝐹 ) ·ih 𝐵 ) = 0 )