Step | Hyp | Ref
| Expression |
1 | | fourierdlem53.xps |
. . . . . . 7
β’ ((π β§ π β π΄) β (π + π ) β π΅) |
2 | | fourierdlem53.1 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
3 | | fourierdlem53.b |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
4 | 2, 3 | fssresd 6748 |
. . . . . . . . . 10
β’ (π β (πΉ βΎ π΅):π΅βΆβ) |
5 | 4 | fdmd 6718 |
. . . . . . . . 9
β’ (π β dom (πΉ βΎ π΅) = π΅) |
6 | 5 | eqcomd 2730 |
. . . . . . . 8
β’ (π β π΅ = dom (πΉ βΎ π΅)) |
7 | 6 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β π΄) β π΅ = dom (πΉ βΎ π΅)) |
8 | 1, 7 | eleqtrd 2827 |
. . . . . 6
β’ ((π β§ π β π΄) β (π + π ) β dom (πΉ βΎ π΅)) |
9 | | fourierdlem53.2 |
. . . . . . . . . . 11
β’ (π β π β β) |
10 | 9 | recnd 11239 |
. . . . . . . . . 10
β’ (π β π β β) |
11 | 10 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π β β) |
12 | | fourierdlem53.3 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
13 | 12 | sselda 3974 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π β β) |
14 | 13 | recnd 11239 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π β β) |
15 | | fourierdlem53.d |
. . . . . . . . . 10
β’ (π β π· β β) |
16 | 15 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π· β β) |
17 | | fourierdlem53.sned |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π β π·) |
18 | 11, 14, 16, 17 | addneintrd 11418 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π + π ) β (π + π·)) |
19 | 18 | neneqd 2937 |
. . . . . . 7
β’ ((π β§ π β π΄) β Β¬ (π + π ) = (π + π·)) |
20 | 9 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β π β β) |
21 | 20, 13 | readdcld 11240 |
. . . . . . . 8
β’ ((π β§ π β π΄) β (π + π ) β β) |
22 | | elsng 4634 |
. . . . . . . 8
β’ ((π + π ) β β β ((π + π ) β {(π + π·)} β (π + π ) = (π + π·))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π΄) β ((π + π ) β {(π + π·)} β (π + π ) = (π + π·))) |
24 | 19, 23 | mtbird 325 |
. . . . . 6
β’ ((π β§ π β π΄) β Β¬ (π + π ) β {(π + π·)}) |
25 | 8, 24 | eldifd 3951 |
. . . . 5
β’ ((π β§ π β π΄) β (π + π ) β (dom (πΉ βΎ π΅) β {(π + π·)})) |
26 | 25 | ralrimiva 3138 |
. . . 4
β’ (π β βπ β π΄ (π + π ) β (dom (πΉ βΎ π΅) β {(π + π·)})) |
27 | | eqid 2724 |
. . . . 5
β’ (π β π΄ β¦ (π + π )) = (π β π΄ β¦ (π + π )) |
28 | 27 | rnmptss 7114 |
. . . 4
β’
(βπ β
π΄ (π + π ) β (dom (πΉ βΎ π΅) β {(π + π·)}) β ran (π β π΄ β¦ (π + π )) β (dom (πΉ βΎ π΅) β {(π + π·)})) |
29 | 26, 28 | syl 17 |
. . 3
β’ (π β ran (π β π΄ β¦ (π + π )) β (dom (πΉ βΎ π΅) β {(π + π·)})) |
30 | | eqid 2724 |
. . . 4
β’ (π β π΄ β¦ π) = (π β π΄ β¦ π) |
31 | | eqid 2724 |
. . . 4
β’ (π β π΄ β¦ π ) = (π β π΄ β¦ π ) |
32 | | ax-resscn 11163 |
. . . . . 6
β’ β
β β |
33 | 12, 32 | sstrdi 3986 |
. . . . 5
β’ (π β π΄ β β) |
34 | 30, 33, 10, 15 | constlimc 44825 |
. . . 4
β’ (π β π β ((π β π΄ β¦ π) limβ π·)) |
35 | 33, 31, 15 | idlimc 44827 |
. . . 4
β’ (π β π· β ((π β π΄ β¦ π ) limβ π·)) |
36 | 30, 31, 27, 11, 14, 34, 35 | addlimc 44849 |
. . 3
β’ (π β (π + π·) β ((π β π΄ β¦ (π + π )) limβ π·)) |
37 | | fourierdlem53.c |
. . 3
β’ (π β πΆ β ((πΉ βΎ π΅) limβ (π + π·))) |
38 | 29, 36, 37 | limccog 44821 |
. 2
β’ (π β πΆ β (((πΉ βΎ π΅) β (π β π΄ β¦ (π + π ))) limβ π·)) |
39 | | nfv 1909 |
. . . . . 6
β’
β²π π |
40 | 39, 27, 1 | rnmptssd 44380 |
. . . . 5
β’ (π β ran (π β π΄ β¦ (π + π )) β π΅) |
41 | | cores 6238 |
. . . . 5
β’ (ran
(π β π΄ β¦ (π + π )) β π΅ β ((πΉ βΎ π΅) β (π β π΄ β¦ (π + π ))) = (πΉ β (π β π΄ β¦ (π + π )))) |
42 | 40, 41 | syl 17 |
. . . 4
β’ (π β ((πΉ βΎ π΅) β (π β π΄ β¦ (π + π ))) = (πΉ β (π β π΄ β¦ (π + π )))) |
43 | 21, 27 | fmptd 7105 |
. . . . 5
β’ (π β (π β π΄ β¦ (π + π )):π΄βΆβ) |
44 | | fcompt 7123 |
. . . . 5
β’ ((πΉ:ββΆβ β§
(π β π΄ β¦ (π + π )):π΄βΆβ) β (πΉ β (π β π΄ β¦ (π + π ))) = (π₯ β π΄ β¦ (πΉβ((π β π΄ β¦ (π + π ))βπ₯)))) |
45 | 2, 43, 44 | syl2anc 583 |
. . . 4
β’ (π β (πΉ β (π β π΄ β¦ (π + π ))) = (π₯ β π΄ β¦ (πΉβ((π β π΄ β¦ (π + π ))βπ₯)))) |
46 | | fourierdlem53.g |
. . . . . 6
β’ πΊ = (π β π΄ β¦ (πΉβ(π + π ))) |
47 | 46 | a1i 11 |
. . . . 5
β’ (π β πΊ = (π β π΄ β¦ (πΉβ(π + π )))) |
48 | | oveq2 7409 |
. . . . . . . 8
β’ (π = π₯ β (π + π ) = (π + π₯)) |
49 | 48 | fveq2d 6885 |
. . . . . . 7
β’ (π = π₯ β (πΉβ(π + π )) = (πΉβ(π + π₯))) |
50 | 49 | cbvmptv 5251 |
. . . . . 6
β’ (π β π΄ β¦ (πΉβ(π + π ))) = (π₯ β π΄ β¦ (πΉβ(π + π₯))) |
51 | 50 | a1i 11 |
. . . . 5
β’ (π β (π β π΄ β¦ (πΉβ(π + π ))) = (π₯ β π΄ β¦ (πΉβ(π + π₯)))) |
52 | | eqidd 2725 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (π β π΄ β¦ (π + π )) = (π β π΄ β¦ (π + π ))) |
53 | 48 | adantl 481 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ π = π₯) β (π + π ) = (π + π₯)) |
54 | | simpr 484 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
55 | 9 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β π β β) |
56 | 12 | sselda 3974 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β π₯ β β) |
57 | 55, 56 | readdcld 11240 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (π + π₯) β β) |
58 | 52, 53, 54, 57 | fvmptd 6995 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((π β π΄ β¦ (π + π ))βπ₯) = (π + π₯)) |
59 | 58 | eqcomd 2730 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (π + π₯) = ((π β π΄ β¦ (π + π ))βπ₯)) |
60 | 59 | fveq2d 6885 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (πΉβ(π + π₯)) = (πΉβ((π β π΄ β¦ (π + π ))βπ₯))) |
61 | 60 | mpteq2dva 5238 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (πΉβ(π + π₯))) = (π₯ β π΄ β¦ (πΉβ((π β π΄ β¦ (π + π ))βπ₯)))) |
62 | 47, 51, 61 | 3eqtrrd 2769 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (πΉβ((π β π΄ β¦ (π + π ))βπ₯))) = πΊ) |
63 | 42, 45, 62 | 3eqtrd 2768 |
. . 3
β’ (π β ((πΉ βΎ π΅) β (π β π΄ β¦ (π + π ))) = πΊ) |
64 | 63 | oveq1d 7416 |
. 2
β’ (π β (((πΉ βΎ π΅) β (π β π΄ β¦ (π + π ))) limβ π·) = (πΊ limβ π·)) |
65 | 38, 64 | eleqtrd 2827 |
1
β’ (π β πΆ β (πΊ limβ π·)) |