Step | Hyp | Ref
| Expression |
1 | | fourierdlem53.xps |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ 𝐵) |
2 | | fourierdlem53.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
3 | | fourierdlem53.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | 2, 3 | fssresd 6538 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℝ) |
5 | 4 | fdmd 6516 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐹 ↾ 𝐵) = 𝐵) |
6 | 5 | eqcomd 2825 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = dom (𝐹 ↾ 𝐵)) |
7 | 6 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐵 = dom (𝐹 ↾ 𝐵)) |
8 | 1, 7 | eleqtrd 2913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ dom (𝐹 ↾ 𝐵)) |
9 | | fourierdlem53.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℝ) |
10 | 9 | recnd 10661 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
11 | 10 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℂ) |
12 | | fourierdlem53.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
13 | 12 | sselda 3965 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
14 | 13 | recnd 10661 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ) |
15 | | fourierdlem53.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
16 | 15 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐷 ∈ ℂ) |
17 | | fourierdlem53.sned |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 𝐷) |
18 | 11, 14, 16, 17 | addneintrd 10839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ≠ (𝑋 + 𝐷)) |
19 | 18 | neneqd 3019 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) = (𝑋 + 𝐷)) |
20 | 9 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℝ) |
21 | 20, 13 | readdcld 10662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ ℝ) |
22 | | elsng 4573 |
. . . . . . . 8
⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
24 | 19, 23 | mtbird 327 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)}) |
25 | 8, 24 | eldifd 3945 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
26 | 25 | ralrimiva 3180 |
. . . 4
⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
27 | | eqid 2819 |
. . . . 5
⊢ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
28 | 27 | rnmptss 6879 |
. . . 4
⊢
(∀𝑠 ∈
𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)}) → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
29 | 26, 28 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
30 | | eqid 2819 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑋) = (𝑠 ∈ 𝐴 ↦ 𝑋) |
31 | | eqid 2819 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠) |
32 | | ax-resscn 10586 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
33 | 12, 32 | sstrdi 3977 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
34 | 30, 33, 10, 15 | constlimc 41895 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑋) limℂ 𝐷)) |
35 | 33, 31, 15 | idlimc 41897 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑠) limℂ 𝐷)) |
36 | 30, 31, 27, 11, 14, 34, 35 | addlimc 41919 |
. . 3
⊢ (𝜑 → (𝑋 + 𝐷) ∈ ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) limℂ 𝐷)) |
37 | | fourierdlem53.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝑋 + 𝐷))) |
38 | 29, 36, 37 | limccog 41891 |
. 2
⊢ (𝜑 → 𝐶 ∈ (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷)) |
39 | | simpr 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
40 | 27 | elrnmpt 5821 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) → (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ↔ ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠))) |
41 | 40 | adantl 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ↔ ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠))) |
42 | 39, 41 | mpbid 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠)) |
43 | | nfv 1909 |
. . . . . . . . . 10
⊢
Ⅎ𝑠𝜑 |
44 | | nfmpt1 5155 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑠(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
45 | 44 | nfrn 5817 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
46 | 45 | nfcri 2969 |
. . . . . . . . . 10
⊢
Ⅎ𝑠 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
47 | 43, 46 | nfan 1894 |
. . . . . . . . 9
⊢
Ⅎ𝑠(𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
48 | | nfv 1909 |
. . . . . . . . 9
⊢
Ⅎ𝑠 𝑦 ∈ 𝐵 |
49 | | simp3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → 𝑦 = (𝑋 + 𝑠)) |
50 | 1 | 3adant3 1127 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → (𝑋 + 𝑠) ∈ 𝐵) |
51 | 49, 50 | eqeltrd 2911 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → 𝑦 ∈ 𝐵) |
52 | 51 | 3exp 1114 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 → (𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵))) |
53 | 52 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (𝑠 ∈ 𝐴 → (𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵))) |
54 | 47, 48, 53 | rexlimd 3315 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵)) |
55 | 42, 54 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → 𝑦 ∈ 𝐵) |
56 | 55 | ralrimiva 3180 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))𝑦 ∈ 𝐵) |
57 | | dfss3 3954 |
. . . . . 6
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 ↔ ∀𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))𝑦 ∈ 𝐵) |
58 | 56, 57 | sylibr 236 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵) |
59 | | cores 6095 |
. . . . 5
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
60 | 58, 59 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
61 | 21, 27 | fmptd 6871 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) |
62 | | fcompt 6888 |
. . . . 5
⊢ ((𝐹:ℝ⟶ℝ ∧
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
63 | 2, 61, 62 | syl2anc 586 |
. . . 4
⊢ (𝜑 → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
64 | | fourierdlem53.g |
. . . . . 6
⊢ 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) |
65 | 64 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠)))) |
66 | | oveq2 7156 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
67 | 66 | fveq2d 6667 |
. . . . . . 7
⊢ (𝑠 = 𝑥 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑥))) |
68 | 67 | cbvmptv 5160 |
. . . . . 6
⊢ (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) |
69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥)))) |
70 | | eqidd 2820 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
71 | 66 | adantl 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑠 = 𝑥) → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
72 | | simpr 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
73 | 9 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ ℝ) |
74 | 12 | sselda 3965 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
75 | 73, 74 | readdcld 10662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) ∈ ℝ) |
76 | 70, 71, 72, 75 | fvmptd 6768 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥) = (𝑋 + 𝑥)) |
77 | 76 | eqcomd 2825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) = ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)) |
78 | 77 | fveq2d 6667 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑥)) = (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) |
79 | 78 | mpteq2dva 5152 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
80 | 65, 69, 79 | 3eqtrrd 2859 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) = 𝐺) |
81 | 60, 63, 80 | 3eqtrd 2858 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = 𝐺) |
82 | 81 | oveq1d 7163 |
. 2
⊢ (𝜑 → (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷) = (𝐺 limℂ 𝐷)) |
83 | 38, 82 | eleqtrd 2913 |
1
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) |