This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> F : RR --> RR )
fourierdlem53.2 
|- ( ph -> X e. RR )
fourierdlem53.3 
|- ( ph -> A C_ RR )
fourierdlem53.g 
|- G = ( s e. A |-> ( F ` ( X + s ) ) )
fourierdlem53.xps 
|- ( ( ph /\ s e. A ) -> ( X + s ) e. B )
fourierdlem53.b 
|- ( ph -> B C_ RR )
fourierdlem53.sned 
|- ( ( ph /\ s e. A ) -> s =/= D )
fourierdlem53.c 
|- ( ph -> C e. ( ( F |` B ) limCC ( X + D ) ) )
fourierdlem53.d 
|- ( ph -> D e. CC )
Assertion fourierdlem53 
|- ( ph -> C e. ( G limCC D ) )

Proof

Step Hyp Ref Expression
1 fourierdlem53.1 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem53.2 
 |-  ( ph -> X e. RR )
3 fourierdlem53.3 
 |-  ( ph -> A C_ RR )
4 fourierdlem53.g 
 |-  G = ( s e. A |-> ( F ` ( X + s ) ) )
5 fourierdlem53.xps 
 |-  ( ( ph /\ s e. A ) -> ( X + s ) e. B )
6 fourierdlem53.b 
 |-  ( ph -> B C_ RR )
7 fourierdlem53.sned 
 |-  ( ( ph /\ s e. A ) -> s =/= D )
8 fourierdlem53.c 
 |-  ( ph -> C e. ( ( F |` B ) limCC ( X + D ) ) )
9 fourierdlem53.d 
 |-  ( ph -> D e. CC )
10 1 6 fssresd 
 |-  ( ph -> ( F |` B ) : B --> RR )
11 10 fdmd 
 |-  ( ph -> dom ( F |` B ) = B )
12 11 eqcomd 
 |-  ( ph -> B = dom ( F |` B ) )
13 12 adantr 
 |-  ( ( ph /\ s e. A ) -> B = dom ( F |` B ) )
14 5 13 eleqtrd 
 |-  ( ( ph /\ s e. A ) -> ( X + s ) e. dom ( F |` B ) )
15 2 recnd 
 |-  ( ph -> X e. CC )
16 15 adantr 
 |-  ( ( ph /\ s e. A ) -> X e. CC )
17 3 sselda 
 |-  ( ( ph /\ s e. A ) -> s e. RR )
18 17 recnd 
 |-  ( ( ph /\ s e. A ) -> s e. CC )
19 9 adantr 
 |-  ( ( ph /\ s e. A ) -> D e. CC )
20 16 18 19 7 addneintrd 
 |-  ( ( ph /\ s e. A ) -> ( X + s ) =/= ( X + D ) )
21 20 neneqd 
 |-  ( ( ph /\ s e. A ) -> -. ( X + s ) = ( X + D ) )
22 2 adantr 
 |-  ( ( ph /\ s e. A ) -> X e. RR )
23 22 17 readdcld 
 |-  ( ( ph /\ s e. A ) -> ( X + s ) e. RR )
24 elsng 
 |-  ( ( X + s ) e. RR -> ( ( X + s ) e. { ( X + D ) } <-> ( X + s ) = ( X + D ) ) )
25 23 24 syl 
 |-  ( ( ph /\ s e. A ) -> ( ( X + s ) e. { ( X + D ) } <-> ( X + s ) = ( X + D ) ) )
26 21 25 mtbird 
 |-  ( ( ph /\ s e. A ) -> -. ( X + s ) e. { ( X + D ) } )
27 14 26 eldifd 
 |-  ( ( ph /\ s e. A ) -> ( X + s ) e. ( dom ( F |` B ) \ { ( X + D ) } ) )
28 27 ralrimiva 
 |-  ( ph -> A. s e. A ( X + s ) e. ( dom ( F |` B ) \ { ( X + D ) } ) )
29 eqid 
 |-  ( s e. A |-> ( X + s ) ) = ( s e. A |-> ( X + s ) )
30 29 rnmptss 
 |-  ( A. s e. A ( X + s ) e. ( dom ( F |` B ) \ { ( X + D ) } ) -> ran ( s e. A |-> ( X + s ) ) C_ ( dom ( F |` B ) \ { ( X + D ) } ) )
31 28 30 syl 
 |-  ( ph -> ran ( s e. A |-> ( X + s ) ) C_ ( dom ( F |` B ) \ { ( X + D ) } ) )
32 eqid 
 |-  ( s e. A |-> X ) = ( s e. A |-> X )
33 eqid 
 |-  ( s e. A |-> s ) = ( s e. A |-> s )
34 ax-resscn 
 |-  RR C_ CC
35 3 34 sstrdi 
 |-  ( ph -> A C_ CC )
36 32 35 15 9 constlimc 
 |-  ( ph -> X e. ( ( s e. A |-> X ) limCC D ) )
37 35 33 9 idlimc 
 |-  ( ph -> D e. ( ( s e. A |-> s ) limCC D ) )
38 32 33 29 16 18 36 37 addlimc 
 |-  ( ph -> ( X + D ) e. ( ( s e. A |-> ( X + s ) ) limCC D ) )
39 31 38 8 limccog 
 |-  ( ph -> C e. ( ( ( F |` B ) o. ( s e. A |-> ( X + s ) ) ) limCC D ) )
40 nfv 
 |-  F/ s ph
41 40 29 5 rnmptssd 
 |-  ( ph -> ran ( s e. A |-> ( X + s ) ) C_ B )
42 cores 
 |-  ( ran ( s e. A |-> ( X + s ) ) C_ B -> ( ( F |` B ) o. ( s e. A |-> ( X + s ) ) ) = ( F o. ( s e. A |-> ( X + s ) ) ) )
43 41 42 syl 
 |-  ( ph -> ( ( F |` B ) o. ( s e. A |-> ( X + s ) ) ) = ( F o. ( s e. A |-> ( X + s ) ) ) )
44 23 29 fmptd 
 |-  ( ph -> ( s e. A |-> ( X + s ) ) : A --> RR )
45 fcompt 
 |-  ( ( F : RR --> RR /\ ( s e. A |-> ( X + s ) ) : A --> RR ) -> ( F o. ( s e. A |-> ( X + s ) ) ) = ( x e. A |-> ( F ` ( ( s e. A |-> ( X + s ) ) ` x ) ) ) )
46 1 44 45 syl2anc 
 |-  ( ph -> ( F o. ( s e. A |-> ( X + s ) ) ) = ( x e. A |-> ( F ` ( ( s e. A |-> ( X + s ) ) ` x ) ) ) )
47 4 a1i 
 |-  ( ph -> G = ( s e. A |-> ( F ` ( X + s ) ) ) )
48 oveq2 
 |-  ( s = x -> ( X + s ) = ( X + x ) )
49 48 fveq2d 
 |-  ( s = x -> ( F ` ( X + s ) ) = ( F ` ( X + x ) ) )
50 49 cbvmptv 
 |-  ( s e. A |-> ( F ` ( X + s ) ) ) = ( x e. A |-> ( F ` ( X + x ) ) )
51 50 a1i 
 |-  ( ph -> ( s e. A |-> ( F ` ( X + s ) ) ) = ( x e. A |-> ( F ` ( X + x ) ) ) )
52 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( s e. A |-> ( X + s ) ) = ( s e. A |-> ( X + s ) ) )
53 48 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ s = x ) -> ( X + s ) = ( X + x ) )
54 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
55 2 adantr 
 |-  ( ( ph /\ x e. A ) -> X e. RR )
56 3 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
57 55 56 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( X + x ) e. RR )
58 52 53 54 57 fvmptd 
 |-  ( ( ph /\ x e. A ) -> ( ( s e. A |-> ( X + s ) ) ` x ) = ( X + x ) )
59 58 eqcomd 
 |-  ( ( ph /\ x e. A ) -> ( X + x ) = ( ( s e. A |-> ( X + s ) ) ` x ) )
60 59 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( F ` ( X + x ) ) = ( F ` ( ( s e. A |-> ( X + s ) ) ` x ) ) )
61 60 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( F ` ( X + x ) ) ) = ( x e. A |-> ( F ` ( ( s e. A |-> ( X + s ) ) ` x ) ) ) )
62 47 51 61 3eqtrrd 
 |-  ( ph -> ( x e. A |-> ( F ` ( ( s e. A |-> ( X + s ) ) ` x ) ) ) = G )
63 43 46 62 3eqtrd 
 |-  ( ph -> ( ( F |` B ) o. ( s e. A |-> ( X + s ) ) ) = G )
64 63 oveq1d 
 |-  ( ph -> ( ( ( F |` B ) o. ( s e. A |-> ( X + s ) ) ) limCC D ) = ( G limCC D ) )
65 39 64 eleqtrd 
 |-  ( ph -> C e. ( G limCC D ) )