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 )