Step | Hyp | Ref
| Expression |
1 | | fourierdlem53.xps |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ 𝐵) |
2 | | fourierdlem53.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
3 | | fourierdlem53.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | 2, 3 | fssresd 6071 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℝ) |
5 | | fdm 6051 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝐵):𝐵⟶ℝ → dom (𝐹 ↾ 𝐵) = 𝐵) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐹 ↾ 𝐵) = 𝐵) |
7 | 6 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = dom (𝐹 ↾ 𝐵)) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐵 = dom (𝐹 ↾ 𝐵)) |
9 | 1, 8 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ dom (𝐹 ↾ 𝐵)) |
10 | | fourierdlem53.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℝ) |
11 | 10 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
12 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℂ) |
13 | | fourierdlem53.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
14 | 13 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
15 | 14 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ) |
16 | | fourierdlem53.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
17 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝐷 ∈ ℂ) |
18 | | fourierdlem53.sned |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 𝐷) |
19 | 12, 15, 17, 18 | addneintrd 10243 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ≠ (𝑋 + 𝐷)) |
20 | 19 | neneqd 2799 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) = (𝑋 + 𝐷)) |
21 | 10 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑋 ∈ ℝ) |
22 | 21, 14 | readdcld 10069 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ ℝ) |
23 | | elsng 4191 |
. . . . . . . 8
⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)} ↔ (𝑋 + 𝑠) = (𝑋 + 𝐷))) |
25 | 20, 24 | mtbird 315 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (𝑋 + 𝑠) ∈ {(𝑋 + 𝐷)}) |
26 | 9, 25 | eldifd 3585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
27 | 26 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
28 | | eqid 2622 |
. . . . 5
⊢ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
29 | 28 | rnmptss 6392 |
. . . 4
⊢
(∀𝑠 ∈
𝐴 (𝑋 + 𝑠) ∈ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)}) → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
30 | 27, 29 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ (dom (𝐹 ↾ 𝐵) ∖ {(𝑋 + 𝐷)})) |
31 | | eqid 2622 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑋) = (𝑠 ∈ 𝐴 ↦ 𝑋) |
32 | | eqid 2622 |
. . . 4
⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠) |
33 | | ax-resscn 9993 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
34 | 13, 33 | syl6ss 3615 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
35 | 31, 34, 11, 16 | constlimc 39856 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑋) limℂ 𝐷)) |
36 | 34, 32, 16 | idlimc 39858 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ((𝑠 ∈ 𝐴 ↦ 𝑠) limℂ 𝐷)) |
37 | 31, 32, 28, 12, 15, 35, 36 | addlimc 39880 |
. . 3
⊢ (𝜑 → (𝑋 + 𝐷) ∈ ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) limℂ 𝐷)) |
38 | | fourierdlem53.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝑋 + 𝐷))) |
39 | 30, 37, 38 | limccog 39852 |
. 2
⊢ (𝜑 → 𝐶 ∈ (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷)) |
40 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
41 | 28 | elrnmpt 5372 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) → (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ↔ ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠))) |
42 | 41 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ↔ ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠))) |
43 | 40, 42 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → ∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠)) |
44 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑠𝜑 |
45 | | nfmpt1 4747 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑠(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
46 | 45 | nfrn 5368 |
. . . . . . . . . . 11
⊢
Ⅎ𝑠ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
47 | 46 | nfcri 2758 |
. . . . . . . . . 10
⊢
Ⅎ𝑠 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) |
48 | 44, 47 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑠(𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
49 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑠 𝑦 ∈ 𝐵 |
50 | | simp3 1063 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → 𝑦 = (𝑋 + 𝑠)) |
51 | 1 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → (𝑋 + 𝑠) ∈ 𝐵) |
52 | 50, 51 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴 ∧ 𝑦 = (𝑋 + 𝑠)) → 𝑦 ∈ 𝐵) |
53 | 52 | 3exp 1264 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 → (𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵))) |
54 | 53 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (𝑠 ∈ 𝐴 → (𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵))) |
55 | 48, 49, 54 | rexlimd 3026 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → (∃𝑠 ∈ 𝐴 𝑦 = (𝑋 + 𝑠) → 𝑦 ∈ 𝐵)) |
56 | 43, 55 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) → 𝑦 ∈ 𝐵) |
57 | 56 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))𝑦 ∈ 𝐵) |
58 | | dfss3 3592 |
. . . . . 6
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 ↔ ∀𝑦 ∈ ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))𝑦 ∈ 𝐵) |
59 | 57, 58 | sylibr 224 |
. . . . 5
⊢ (𝜑 → ran (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵) |
60 | | cores 5638 |
. . . . 5
⊢ (ran
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
61 | 59, 60 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)))) |
62 | 22, 28 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) |
63 | | fcompt 6400 |
. . . . 5
⊢ ((𝐹:ℝ⟶ℝ ∧
(𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)):𝐴⟶ℝ) → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
64 | 2, 62, 63 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐹 ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
65 | | fourierdlem53.g |
. . . . . 6
⊢ 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) |
66 | 65 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠)))) |
67 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑠 = 𝑥 → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
68 | 67 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑠 = 𝑥 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑥))) |
69 | 68 | cbvmptv 4750 |
. . . . . 6
⊢ (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) |
70 | 69 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥)))) |
71 | | eqidd 2623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠)) = (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) |
72 | 67 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑠 = 𝑥) → (𝑋 + 𝑠) = (𝑋 + 𝑥)) |
73 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
74 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑋 ∈ ℝ) |
75 | 13 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
76 | 74, 75 | readdcld 10069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) ∈ ℝ) |
77 | 71, 72, 73, 76 | fvmptd 6288 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥) = (𝑋 + 𝑥)) |
78 | 77 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋 + 𝑥) = ((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)) |
79 | 78 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋 + 𝑥)) = (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) |
80 | 79 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥)))) |
81 | 66, 70, 80 | 3eqtrrd 2661 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘((𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))‘𝑥))) = 𝐺) |
82 | 61, 64, 81 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) = 𝐺) |
83 | 82 | oveq1d 6665 |
. 2
⊢ (𝜑 → (((𝐹 ↾ 𝐵) ∘ (𝑠 ∈ 𝐴 ↦ (𝑋 + 𝑠))) limℂ 𝐷) = (𝐺 limℂ 𝐷)) |
84 | 39, 83 | eleqtrd 2703 |
1
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) |