Step | Hyp | Ref
| Expression |
1 | | fourierdlem53.xps |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ 𝐵) |
2 | | fourierdlem53.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
3 | | fourierdlem53.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | 2, 3 | fssresd 6641 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℝ) |
5 | 4 | fdmd 6611 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐹 ↾ 𝐵) = 𝐵) |
6 | 5 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = dom (𝐹 ↾ 𝐵)) |
7 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐵 = dom (𝐹 ↾ 𝐵)) |
8 | 1, 7 | eleqtrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ dom (𝐹 ↾ 𝐵)) |
9 | | fourierdlem53.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℝ) |
10 | 9 | recnd 11003 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
11 | 10 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℂ) |
12 | | fourierdlem53.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
13 | 12 | sselda 3921 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
14 | 13 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ) |
15 | | fourierdlem53.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
16 | 15 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐷 ∈ ℂ) |
17 | | fourierdlem53.sned |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 𝐷) |
18 | 11, 14, 16, 17 | addneintrd 11182 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ≠ (𝑋 + 𝐷)) |
19 | 18 | neneqd 2948 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) = (𝑋 + 𝐷)) |
20 | 9 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℝ) |
21 | 20, 13 | readdcld 11004 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ ℝ) |
22 | | elsng 4575 |
. . . . . . . 8
⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
24 | 19, 23 | mtbird 325 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)}) |
25 | 8, 24 | eldifd 3898 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
26 | 25 | ralrimiva 3103 |
. . . 4
⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
27 | | eqid 2738 |
. . . . 5
⊢ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
28 | 27 | rnmptss 6996 |
. . . 4
⊢
(∀𝑠 ∈
𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)}) → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
29 | 26, 28 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
30 | | eqid 2738 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑋) = (𝑠 ∈ 𝐴 ↦ 𝑋) |
31 | | eqid 2738 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠) |
32 | | ax-resscn 10928 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
33 | 12, 32 | sstrdi 3933 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
34 | 30, 33, 10, 15 | constlimc 43165 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑋) limℂ 𝐷)) |
35 | 33, 31, 15 | idlimc 43167 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑠) limℂ 𝐷)) |
36 | 30, 31, 27, 11, 14, 34, 35 | addlimc 43189 |
. . 3
⊢ (𝜑 → (𝑋 + 𝐷) ∈ ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) limℂ 𝐷)) |
37 | | fourierdlem53.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝑋 + 𝐷))) |
38 | 29, 36, 37 | limccog 43161 |
. 2
⊢ (𝜑 → 𝐶 ∈ (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷)) |
39 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑠𝜑 |
40 | 39, 27, 1 | rnmptssd 42735 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵) |
41 | | cores 6153 |
. . . . 5
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
42 | 40, 41 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
43 | 21, 27 | fmptd 6988 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) |
44 | | fcompt 7005 |
. . . . 5
⊢ ((𝐹:ℝ⟶ℝ ∧
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
45 | 2, 43, 44 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
46 | | fourierdlem53.g |
. . . . . 6
⊢ 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) |
47 | 46 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠)))) |
48 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
49 | 48 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑠 = 𝑥 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑥))) |
50 | 49 | cbvmptv 5187 |
. . . . . 6
⊢ (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) |
51 | 50 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥)))) |
52 | | eqidd 2739 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
53 | 48 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑠 = 𝑥) → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
54 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
55 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ ℝ) |
56 | 12 | sselda 3921 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
57 | 55, 56 | readdcld 11004 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) ∈ ℝ) |
58 | 52, 53, 54, 57 | fvmptd 6882 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥) = (𝑋 + 𝑥)) |
59 | 58 | eqcomd 2744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) = ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)) |
60 | 59 | fveq2d 6778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑥)) = (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) |
61 | 60 | mpteq2dva 5174 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
62 | 47, 51, 61 | 3eqtrrd 2783 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) = 𝐺) |
63 | 42, 45, 62 | 3eqtrd 2782 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = 𝐺) |
64 | 63 | oveq1d 7290 |
. 2
⊢ (𝜑 → (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷) = (𝐺 limℂ 𝐷)) |
65 | 38, 64 | eleqtrd 2841 |
1
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) |