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 ffvelcdmda ⊒ ( ( πœ‘ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ ( βŠ₯ β€˜ 𝐴 ) )
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 )