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 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem53.2 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem53.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
fourierdlem53.g ⊢ 𝐺 = ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
fourierdlem53.xps ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ 𝐵 )
fourierdlem53.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
fourierdlem53.sned ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≠ 𝐷 )
fourierdlem53.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ ( 𝑋 + 𝐷 ) ) )
fourierdlem53.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
Assertion fourierdlem53 ( 𝜑 → 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem53.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem53.2 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3 fourierdlem53.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 fourierdlem53.g ⊢ 𝐺 = ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
5 fourierdlem53.xps ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ 𝐵 )
6 fourierdlem53.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
7 fourierdlem53.sned ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≠ 𝐷 )
8 fourierdlem53.c ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ ( 𝑋 + 𝐷 ) ) )
9 fourierdlem53.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
10 1 6 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℝ )
11 10 fdmd ⊢ ( 𝜑 → dom ( 𝐹 ↾ 𝐵 ) = 𝐵 )
12 11 eqcomd ⊢ ( 𝜑 → 𝐵 = dom ( 𝐹 ↾ 𝐵 ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐵 = dom ( 𝐹 ↾ 𝐵 ) )
14 5 13 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ dom ( 𝐹 ↾ 𝐵 ) )
15 2 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℂ )
17 3 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℝ )
18 17 recnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ℂ )
19 9 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
20 16 18 19 7 addneintrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ≠ ( 𝑋 + 𝐷 ) )
21 20 neneqd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝐷 ) )
22 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
23 22 17 readdcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
24 elsng ⊢ ( ( 𝑋 + 𝑠 ) ∈ ℝ → ( ( 𝑋 + 𝑠 ) ∈ { ( 𝑋 + 𝐷 ) } ↔ ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝐷 ) ) )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑋 + 𝑠 ) ∈ { ( 𝑋 + 𝐷 ) } ↔ ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝐷 ) ) )
26 21 25 mtbird ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ¬ ( 𝑋 + 𝑠 ) ∈ { ( 𝑋 + 𝐷 ) } )
27 14 26 eldifd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑋 + 𝑠 ) ∈ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐴 ( 𝑋 + 𝑠 ) ∈ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
29 eqid ⊢ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) )
30 29 rnmptss ⊢ ( ∀ 𝑠 ∈ 𝐴 ( 𝑋 + 𝑠 ) ∈ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) → ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
31 28 30 syl ⊢ ( 𝜑 → ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ ( dom ( 𝐹 ↾ 𝐵 ) ∖ { ( 𝑋 + 𝐷 ) } ) )
32 eqid ⊢ ( 𝑠 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑠 ∈ 𝐴 ↦ 𝑋 )
33 eqid ⊢ ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) = ( 𝑠 ∈ 𝐴 ↦ 𝑠 )
34 ax-resscn ⊢ ℝ ⊆ ℂ
35 3 34 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
36 32 35 15 9 constlimc ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑠 ∈ 𝐴 ↦ 𝑋 ) limℂ 𝐷 ) )
37 35 33 9 idlimc ⊢ ( 𝜑 → 𝐷 ∈ ( ( 𝑠 ∈ 𝐴 ↦ 𝑠 ) limℂ 𝐷 ) )
38 32 33 29 16 18 36 37 addlimc ⊢ ( 𝜑 → ( 𝑋 + 𝐷 ) ∈ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) limℂ 𝐷 ) )
39 31 38 8 limccog ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) limℂ 𝐷 ) )
40 nfv ⊢ Ⅎ 𝑠 𝜑
41 40 29 5 rnmptssd ⊢ ( 𝜑 → ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ 𝐵 )
42 cores ⊢ ( ran ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) )
43 41 42 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) )
44 23 29 fmptd ⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) : 𝐴 ⟶ ℝ )
45 fcompt ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) : 𝐴 ⟶ ℝ ) → ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) )
46 1 44 45 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) )
47 4 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
48 oveq2 ⊢ ( 𝑠 = 𝑥 → ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝑥 ) )
49 48 fveq2d ⊢ ( 𝑠 = 𝑥 → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) )
50 49 cbvmptv ⊢ ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) )
51 50 a1i ⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) ) )
52 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) = ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) )
53 48 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑠 = 𝑥 ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝑥 ) )
54 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
55 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ∈ ℝ )
56 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
57 55 56 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑋 + 𝑥 ) ∈ ℝ )
58 52 53 54 57 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) = ( 𝑋 + 𝑥 ) )
59 58 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑋 + 𝑥 ) = ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) )
60 59 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) = ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) )
61 60 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝑋 + 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) )
62 47 51 61 3eqtrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ‘ 𝑥 ) ) ) = 𝐺 )
63 43 46 62 3eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) = 𝐺 )
64 63 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐵 ) ∘ ( 𝑠 ∈ 𝐴 ↦ ( 𝑋 + 𝑠 ) ) ) limℂ 𝐷 ) = ( 𝐺 limℂ 𝐷 ) )
65 39 64 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 limℂ 𝐷 ) )