# Metamath Proof Explorer

## Theorem fourierdlem53

Description: The limit of F ( s ) at ( X + D ) is the limit of F ( X + s ) at D . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem53.1 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem53.2 ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem53.3 ${⊢}{\phi }\to {A}\subseteq ℝ$
fourierdlem53.g ${⊢}{G}=\left({s}\in {A}⟼{F}\left({X}+{s}\right)\right)$
fourierdlem53.xps ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\in {B}$
fourierdlem53.b ${⊢}{\phi }\to {B}\subseteq ℝ$
fourierdlem53.sned ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {s}\ne {D}$
fourierdlem53.c ${⊢}{\phi }\to {C}\in \left(\left({{F}↾}_{{B}}\right){lim}_{ℂ}\left({X}+{D}\right)\right)$
fourierdlem53.d ${⊢}{\phi }\to {D}\in ℂ$
Assertion fourierdlem53 ${⊢}{\phi }\to {C}\in \left({G}{lim}_{ℂ}{D}\right)$

### Proof

Step Hyp Ref Expression
1 fourierdlem53.1 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierdlem53.2 ${⊢}{\phi }\to {X}\in ℝ$
3 fourierdlem53.3 ${⊢}{\phi }\to {A}\subseteq ℝ$
4 fourierdlem53.g ${⊢}{G}=\left({s}\in {A}⟼{F}\left({X}+{s}\right)\right)$
5 fourierdlem53.xps ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\in {B}$
6 fourierdlem53.b ${⊢}{\phi }\to {B}\subseteq ℝ$
7 fourierdlem53.sned ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {s}\ne {D}$
8 fourierdlem53.c ${⊢}{\phi }\to {C}\in \left(\left({{F}↾}_{{B}}\right){lim}_{ℂ}\left({X}+{D}\right)\right)$
9 fourierdlem53.d ${⊢}{\phi }\to {D}\in ℂ$
10 1 6 fssresd ${⊢}{\phi }\to \left({{F}↾}_{{B}}\right):{B}⟶ℝ$
11 10 fdmd ${⊢}{\phi }\to \mathrm{dom}\left({{F}↾}_{{B}}\right)={B}$
12 11 eqcomd ${⊢}{\phi }\to {B}=\mathrm{dom}\left({{F}↾}_{{B}}\right)$
13 12 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {B}=\mathrm{dom}\left({{F}↾}_{{B}}\right)$
14 5 13 eleqtrd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\in \mathrm{dom}\left({{F}↾}_{{B}}\right)$
15 2 recnd ${⊢}{\phi }\to {X}\in ℂ$
16 15 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}\in ℂ$
17 3 sselda ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {s}\in ℝ$
18 17 recnd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {s}\in ℂ$
19 9 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {D}\in ℂ$
20 16 18 19 7 addneintrd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\ne {X}+{D}$
21 20 neneqd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to ¬{X}+{s}={X}+{D}$
22 2 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}\in ℝ$
23 22 17 readdcld ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\in ℝ$
24 elsng ${⊢}{X}+{s}\in ℝ\to \left({X}+{s}\in \left\{{X}+{D}\right\}↔{X}+{s}={X}+{D}\right)$
25 23 24 syl ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to \left({X}+{s}\in \left\{{X}+{D}\right\}↔{X}+{s}={X}+{D}\right)$
26 21 25 mtbird ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to ¬{X}+{s}\in \left\{{X}+{D}\right\}$
27 14 26 eldifd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\in \left(\mathrm{dom}\left({{F}↾}_{{B}}\right)\setminus \left\{{X}+{D}\right\}\right)$
28 27 ralrimiva ${⊢}{\phi }\to \forall {s}\in {A}\phantom{\rule{.4em}{0ex}}{X}+{s}\in \left(\mathrm{dom}\left({{F}↾}_{{B}}\right)\setminus \left\{{X}+{D}\right\}\right)$
29 eqid ${⊢}\left({s}\in {A}⟼{X}+{s}\right)=\left({s}\in {A}⟼{X}+{s}\right)$
30 29 rnmptss ${⊢}\forall {s}\in {A}\phantom{\rule{.4em}{0ex}}{X}+{s}\in \left(\mathrm{dom}\left({{F}↾}_{{B}}\right)\setminus \left\{{X}+{D}\right\}\right)\to \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\subseteq \mathrm{dom}\left({{F}↾}_{{B}}\right)\setminus \left\{{X}+{D}\right\}$
31 28 30 syl ${⊢}{\phi }\to \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\subseteq \mathrm{dom}\left({{F}↾}_{{B}}\right)\setminus \left\{{X}+{D}\right\}$
32 eqid ${⊢}\left({s}\in {A}⟼{X}\right)=\left({s}\in {A}⟼{X}\right)$
33 eqid ${⊢}\left({s}\in {A}⟼{s}\right)=\left({s}\in {A}⟼{s}\right)$
34 ax-resscn ${⊢}ℝ\subseteq ℂ$
35 3 34 sstrdi ${⊢}{\phi }\to {A}\subseteq ℂ$
36 32 35 15 9 constlimc ${⊢}{\phi }\to {X}\in \left(\left({s}\in {A}⟼{X}\right){lim}_{ℂ}{D}\right)$
37 35 33 9 idlimc ${⊢}{\phi }\to {D}\in \left(\left({s}\in {A}⟼{s}\right){lim}_{ℂ}{D}\right)$
38 32 33 29 16 18 36 37 addlimc ${⊢}{\phi }\to {X}+{D}\in \left(\left({s}\in {A}⟼{X}+{s}\right){lim}_{ℂ}{D}\right)$
39 31 38 8 limccog ${⊢}{\phi }\to {C}\in \left(\left(\left({{F}↾}_{{B}}\right)\circ \left({s}\in {A}⟼{X}+{s}\right)\right){lim}_{ℂ}{D}\right)$
40 simpr ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)\to {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)$
41 29 elrnmpt ${⊢}{y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\to \left({y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)↔\exists {s}\in {A}\phantom{\rule{.4em}{0ex}}{y}={X}+{s}\right)$
42 41 adantl ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)\to \left({y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)↔\exists {s}\in {A}\phantom{\rule{.4em}{0ex}}{y}={X}+{s}\right)$
43 40 42 mpbid ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)\to \exists {s}\in {A}\phantom{\rule{.4em}{0ex}}{y}={X}+{s}$
44 nfv ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}{\phi }$
45 nfmpt1 ${⊢}\underset{_}{Ⅎ}{s}\phantom{\rule{.4em}{0ex}}\left({s}\in {A}⟼{X}+{s}\right)$
46 45 nfrn ${⊢}\underset{_}{Ⅎ}{s}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)$
47 46 nfcri ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}{y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)$
48 44 47 nfan ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)$
49 nfv ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
50 simp3 ${⊢}\left({\phi }\wedge {s}\in {A}\wedge {y}={X}+{s}\right)\to {y}={X}+{s}$
51 5 3adant3 ${⊢}\left({\phi }\wedge {s}\in {A}\wedge {y}={X}+{s}\right)\to {X}+{s}\in {B}$
52 50 51 eqeltrd ${⊢}\left({\phi }\wedge {s}\in {A}\wedge {y}={X}+{s}\right)\to {y}\in {B}$
53 52 3exp ${⊢}{\phi }\to \left({s}\in {A}\to \left({y}={X}+{s}\to {y}\in {B}\right)\right)$
54 53 adantr ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)\to \left({s}\in {A}\to \left({y}={X}+{s}\to {y}\in {B}\right)\right)$
55 48 49 54 rexlimd ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)\to \left(\exists {s}\in {A}\phantom{\rule{.4em}{0ex}}{y}={X}+{s}\to {y}\in {B}\right)$
56 43 55 mpd ${⊢}\left({\phi }\wedge {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\right)\to {y}\in {B}$
57 56 ralrimiva ${⊢}{\phi }\to \forall {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\phantom{\rule{.4em}{0ex}}{y}\in {B}$
58 dfss3 ${⊢}\mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\subseteq {B}↔\forall {y}\in \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\phantom{\rule{.4em}{0ex}}{y}\in {B}$
59 57 58 sylibr ${⊢}{\phi }\to \mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\subseteq {B}$
60 cores ${⊢}\mathrm{ran}\left({s}\in {A}⟼{X}+{s}\right)\subseteq {B}\to \left({{F}↾}_{{B}}\right)\circ \left({s}\in {A}⟼{X}+{s}\right)={F}\circ \left({s}\in {A}⟼{X}+{s}\right)$
61 59 60 syl ${⊢}{\phi }\to \left({{F}↾}_{{B}}\right)\circ \left({s}\in {A}⟼{X}+{s}\right)={F}\circ \left({s}\in {A}⟼{X}+{s}\right)$
62 23 29 fmptd ${⊢}{\phi }\to \left({s}\in {A}⟼{X}+{s}\right):{A}⟶ℝ$
63 fcompt ${⊢}\left({F}:ℝ⟶ℝ\wedge \left({s}\in {A}⟼{X}+{s}\right):{A}⟶ℝ\right)\to {F}\circ \left({s}\in {A}⟼{X}+{s}\right)=\left({x}\in {A}⟼{F}\left(\left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)\right)\right)$
64 1 62 63 syl2anc ${⊢}{\phi }\to {F}\circ \left({s}\in {A}⟼{X}+{s}\right)=\left({x}\in {A}⟼{F}\left(\left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)\right)\right)$
65 4 a1i ${⊢}{\phi }\to {G}=\left({s}\in {A}⟼{F}\left({X}+{s}\right)\right)$
66 oveq2 ${⊢}{s}={x}\to {X}+{s}={X}+{x}$
67 66 fveq2d ${⊢}{s}={x}\to {F}\left({X}+{s}\right)={F}\left({X}+{x}\right)$
68 67 cbvmptv ${⊢}\left({s}\in {A}⟼{F}\left({X}+{s}\right)\right)=\left({x}\in {A}⟼{F}\left({X}+{x}\right)\right)$
69 68 a1i ${⊢}{\phi }\to \left({s}\in {A}⟼{F}\left({X}+{s}\right)\right)=\left({x}\in {A}⟼{F}\left({X}+{x}\right)\right)$
70 eqidd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({s}\in {A}⟼{X}+{s}\right)=\left({s}\in {A}⟼{X}+{s}\right)$
71 66 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {A}\right)\wedge {s}={x}\right)\to {X}+{s}={X}+{x}$
72 simpr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in {A}$
73 2 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {X}\in ℝ$
74 3 sselda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in ℝ$
75 73 74 readdcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {X}+{x}\in ℝ$
76 70 71 72 75 fvmptd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)={X}+{x}$
77 76 eqcomd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {X}+{x}=\left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)$
78 77 fveq2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({X}+{x}\right)={F}\left(\left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)\right)$
79 78 mpteq2dva ${⊢}{\phi }\to \left({x}\in {A}⟼{F}\left({X}+{x}\right)\right)=\left({x}\in {A}⟼{F}\left(\left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)\right)\right)$
80 65 69 79 3eqtrrd ${⊢}{\phi }\to \left({x}\in {A}⟼{F}\left(\left({s}\in {A}⟼{X}+{s}\right)\left({x}\right)\right)\right)={G}$
81 61 64 80 3eqtrd ${⊢}{\phi }\to \left({{F}↾}_{{B}}\right)\circ \left({s}\in {A}⟼{X}+{s}\right)={G}$
82 81 oveq1d ${⊢}{\phi }\to \left(\left({{F}↾}_{{B}}\right)\circ \left({s}\in {A}⟼{X}+{s}\right)\right){lim}_{ℂ}{D}={G}{lim}_{ℂ}{D}$
83 39 82 eleqtrd ${⊢}{\phi }\to {C}\in \left({G}{lim}_{ℂ}{D}\right)$