Step | Hyp | Ref
| Expression |
1 | | fourierdlem53.xps |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ 𝐵) |
2 | | fourierdlem53.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
3 | | fourierdlem53.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | 2, 3 | fssresd 6323 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℝ) |
5 | 4 | fdmd 6302 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐹 ↾ 𝐵) = 𝐵) |
6 | 5 | eqcomd 2784 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = dom (𝐹 ↾ 𝐵)) |
7 | 6 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐵 = dom (𝐹 ↾ 𝐵)) |
8 | 1, 7 | eleqtrd 2861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ dom (𝐹 ↾ 𝐵)) |
9 | | fourierdlem53.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℝ) |
10 | 9 | recnd 10407 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
11 | 10 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℂ) |
12 | | fourierdlem53.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
13 | 12 | sselda 3821 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
14 | 13 | recnd 10407 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ) |
15 | | fourierdlem53.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
16 | 15 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐷 ∈ ℂ) |
17 | | fourierdlem53.sned |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 𝐷) |
18 | 11, 14, 16, 17 | addneintrd 10585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ≠ (𝑋 + 𝐷)) |
19 | 18 | neneqd 2974 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) = (𝑋 + 𝐷)) |
20 | 9 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℝ) |
21 | 20, 13 | readdcld 10408 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ ℝ) |
22 | | elsng 4412 |
. . . . . . . 8
⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
24 | 19, 23 | mtbird 317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)}) |
25 | 8, 24 | eldifd 3803 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
26 | 25 | ralrimiva 3148 |
. . . 4
⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
27 | | eqid 2778 |
. . . . 5
⊢ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
28 | 27 | rnmptss 6658 |
. . . 4
⊢
(∀𝑠 ∈
𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)}) → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
29 | 26, 28 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
30 | | eqid 2778 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑋) = (𝑠 ∈ 𝐴 ↦ 𝑋) |
31 | | eqid 2778 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠) |
32 | | ax-resscn 10331 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
33 | 12, 32 | syl6ss 3833 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
34 | 30, 33, 10, 15 | constlimc 40774 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑋) limℂ 𝐷)) |
35 | 33, 31, 15 | idlimc 40776 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑠) limℂ 𝐷)) |
36 | 30, 31, 27, 11, 14, 34, 35 | addlimc 40798 |
. . 3
⊢ (𝜑 → (𝑋 + 𝐷) ∈ ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) limℂ 𝐷)) |
37 | | fourierdlem53.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝑋 + 𝐷))) |
38 | 29, 36, 37 | limccog 40770 |
. 2
⊢ (𝜑 → 𝐶 ∈ (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷)) |
39 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
40 | 27 | elrnmpt 5620 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) → (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ↔ ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠))) |
41 | 40 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ↔ ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠))) |
42 | 39, 41 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠)) |
43 | | nfv 1957 |
. . . . . . . . . 10
⊢
Ⅎ𝑠𝜑 |
44 | | nfmpt1 4984 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑠(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
45 | 44 | nfrn 5616 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
46 | 45 | nfcri 2929 |
. . . . . . . . . 10
⊢
Ⅎ𝑠 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
47 | 43, 46 | nfan 1946 |
. . . . . . . . 9
⊢
Ⅎ𝑠(𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
48 | | nfv 1957 |
. . . . . . . . 9
⊢
Ⅎ𝑠 𝑦 ∈ 𝐵 |
49 | | simp3 1129 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → 𝑦 = (𝑋 + 𝑠)) |
50 | 1 | 3adant3 1123 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → (𝑋 + 𝑠) ∈ 𝐵) |
51 | 49, 50 | eqeltrd 2859 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → 𝑦 ∈ 𝐵) |
52 | 51 | 3exp 1109 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 → (𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵))) |
53 | 52 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (𝑠 ∈ 𝐴 → (𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵))) |
54 | 47, 48, 53 | rexlimd 3208 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵)) |
55 | 42, 54 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → 𝑦 ∈ 𝐵) |
56 | 55 | ralrimiva 3148 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))𝑦 ∈ 𝐵) |
57 | | dfss3 3810 |
. . . . . 6
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 ↔ ∀𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))𝑦 ∈ 𝐵) |
58 | 56, 57 | sylibr 226 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵) |
59 | | cores 5894 |
. . . . 5
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
60 | 58, 59 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
61 | 21, 27 | fmptd 6650 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) |
62 | | fcompt 6667 |
. . . . 5
⊢ ((𝐹:ℝ⟶ℝ ∧
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
63 | 2, 61, 62 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
64 | | fourierdlem53.g |
. . . . . 6
⊢ 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) |
65 | 64 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠)))) |
66 | | oveq2 6932 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
67 | 66 | fveq2d 6452 |
. . . . . . 7
⊢ (𝑠 = 𝑥 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑥))) |
68 | 67 | cbvmptv 4987 |
. . . . . 6
⊢ (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) |
69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥)))) |
70 | | eqidd 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
71 | 66 | adantl 475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑠 = 𝑥) → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
72 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
73 | 9 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ ℝ) |
74 | 12 | sselda 3821 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
75 | 73, 74 | readdcld 10408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) ∈ ℝ) |
76 | 70, 71, 72, 75 | fvmptd 6550 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥) = (𝑋 + 𝑥)) |
77 | 76 | eqcomd 2784 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) = ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)) |
78 | 77 | fveq2d 6452 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑥)) = (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) |
79 | 78 | mpteq2dva 4981 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
80 | 65, 69, 79 | 3eqtrrd 2819 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) = 𝐺) |
81 | 60, 63, 80 | 3eqtrd 2818 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = 𝐺) |
82 | 81 | oveq1d 6939 |
. 2
⊢ (𝜑 → (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷) = (𝐺 limℂ 𝐷)) |
83 | 38, 82 | eleqtrd 2861 |
1
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) |