Step | Hyp | Ref
| Expression |
1 | | dvcmul.a |
. . . 4
β’ (π β π΄ β β) |
2 | | fconst6g 6735 |
. . . 4
β’ (π΄ β β β (π Γ {π΄}):πβΆβ) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β (π Γ {π΄}):πβΆβ) |
4 | | ssidd 3971 |
. . 3
β’ (π β π β π) |
5 | | dvcmul.f |
. . 3
β’ (π β πΉ:πβΆβ) |
6 | | dvcmul.x |
. . 3
β’ (π β π β π) |
7 | | dvcmul.s |
. . 3
β’ (π β π β {β, β}) |
8 | | recnprss 25291 |
. . . . . . . 8
β’ (π β {β, β}
β π β
β) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
10 | 9, 5, 6 | dvbss 25288 |
. . . . . 6
β’ (π β dom (π D πΉ) β π) |
11 | | dvcmul.c |
. . . . . 6
β’ (π β πΆ β dom (π D πΉ)) |
12 | 10, 11 | sseldd 3949 |
. . . . 5
β’ (π β πΆ β π) |
13 | 6, 12 | sseldd 3949 |
. . . 4
β’ (π β πΆ β π) |
14 | | fconst6g 6735 |
. . . . . . . . 9
β’ (π΄ β β β (β
Γ {π΄}):ββΆβ) |
15 | 1, 14 | syl 17 |
. . . . . . . 8
β’ (π β (β Γ {π΄}):ββΆβ) |
16 | | ssidd 3971 |
. . . . . . . 8
β’ (π β β β
β) |
17 | | dvconst 25304 |
. . . . . . . . . . . 12
β’ (π΄ β β β (β
D (β Γ {π΄})) =
(β Γ {0})) |
18 | 1, 17 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β D (β
Γ {π΄})) = (β
Γ {0})) |
19 | 18 | dmeqd 5865 |
. . . . . . . . . 10
β’ (π β dom (β D (β
Γ {π΄})) = dom
(β Γ {0})) |
20 | | c0ex 11157 |
. . . . . . . . . . . 12
β’ 0 β
V |
21 | 20 | fconst 6732 |
. . . . . . . . . . 11
β’ (β
Γ {0}):ββΆ{0} |
22 | 21 | fdmi 6684 |
. . . . . . . . . 10
β’ dom
(β Γ {0}) = β |
23 | 19, 22 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β dom (β D (β
Γ {π΄})) =
β) |
24 | 9, 23 | sseqtrrd 3989 |
. . . . . . . 8
β’ (π β π β dom (β D (β Γ
{π΄}))) |
25 | | dvres3 25300 |
. . . . . . . 8
β’ (((π β {β, β} β§
(β Γ {π΄}):ββΆβ) β§ (β
β β β§ π
β dom (β D (β Γ {π΄})))) β (π D ((β Γ {π΄}) βΎ π)) = ((β D (β Γ {π΄})) βΎ π)) |
26 | 7, 15, 16, 24, 25 | syl22anc 838 |
. . . . . . 7
β’ (π β (π D ((β Γ {π΄}) βΎ π)) = ((β D (β Γ {π΄})) βΎ π)) |
27 | | xpssres 5978 |
. . . . . . . . 9
β’ (π β β β
((β Γ {π΄})
βΎ π) = (π Γ {π΄})) |
28 | 9, 27 | syl 17 |
. . . . . . . 8
β’ (π β ((β Γ {π΄}) βΎ π) = (π Γ {π΄})) |
29 | 28 | oveq2d 7377 |
. . . . . . 7
β’ (π β (π D ((β Γ {π΄}) βΎ π)) = (π D (π Γ {π΄}))) |
30 | 18 | reseq1d 5940 |
. . . . . . . 8
β’ (π β ((β D (β
Γ {π΄})) βΎ π) = ((β Γ {0})
βΎ π)) |
31 | | xpssres 5978 |
. . . . . . . . 9
β’ (π β β β
((β Γ {0}) βΎ π) = (π Γ {0})) |
32 | 9, 31 | syl 17 |
. . . . . . . 8
β’ (π β ((β Γ {0})
βΎ π) = (π Γ {0})) |
33 | 30, 32 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((β D (β
Γ {π΄})) βΎ π) = (π Γ {0})) |
34 | 26, 29, 33 | 3eqtr3d 2781 |
. . . . . 6
β’ (π β (π D (π Γ {π΄})) = (π Γ {0})) |
35 | 20 | fconst2 7158 |
. . . . . 6
β’ ((π D (π Γ {π΄})):πβΆ{0} β (π D (π Γ {π΄})) = (π Γ {0})) |
36 | 34, 35 | sylibr 233 |
. . . . 5
β’ (π β (π D (π Γ {π΄})):πβΆ{0}) |
37 | 36 | fdmd 6683 |
. . . 4
β’ (π β dom (π D (π Γ {π΄})) = π) |
38 | 13, 37 | eleqtrrd 2837 |
. . 3
β’ (π β πΆ β dom (π D (π Γ {π΄}))) |
39 | 3, 4, 5, 6, 7, 38,
11 | dvmul 25328 |
. 2
β’ (π β ((π D ((π Γ {π΄}) βf Β· πΉ))βπΆ) = ((((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) + (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ)))) |
40 | 34 | fveq1d 6848 |
. . . . . 6
β’ (π β ((π D (π Γ {π΄}))βπΆ) = ((π Γ {0})βπΆ)) |
41 | 20 | fvconst2 7157 |
. . . . . . 7
β’ (πΆ β π β ((π Γ {0})βπΆ) = 0) |
42 | 13, 41 | syl 17 |
. . . . . 6
β’ (π β ((π Γ {0})βπΆ) = 0) |
43 | 40, 42 | eqtrd 2773 |
. . . . 5
β’ (π β ((π D (π Γ {π΄}))βπΆ) = 0) |
44 | 43 | oveq1d 7376 |
. . . 4
β’ (π β (((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) = (0 Β· (πΉβπΆ))) |
45 | 5, 12 | ffvelcdmd 7040 |
. . . . 5
β’ (π β (πΉβπΆ) β β) |
46 | 45 | mul02d 11361 |
. . . 4
β’ (π β (0 Β· (πΉβπΆ)) = 0) |
47 | 44, 46 | eqtrd 2773 |
. . 3
β’ (π β (((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) = 0) |
48 | | fvconst2g 7155 |
. . . . . 6
β’ ((π΄ β β β§ πΆ β π) β ((π Γ {π΄})βπΆ) = π΄) |
49 | 1, 13, 48 | syl2anc 585 |
. . . . 5
β’ (π β ((π Γ {π΄})βπΆ) = π΄) |
50 | 49 | oveq2d 7377 |
. . . 4
β’ (π β (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ)) = (((π D πΉ)βπΆ) Β· π΄)) |
51 | | dvfg 25293 |
. . . . . . 7
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
52 | 7, 51 | syl 17 |
. . . . . 6
β’ (π β (π D πΉ):dom (π D πΉ)βΆβ) |
53 | 52, 11 | ffvelcdmd 7040 |
. . . . 5
β’ (π β ((π D πΉ)βπΆ) β β) |
54 | 53, 1 | mulcomd 11184 |
. . . 4
β’ (π β (((π D πΉ)βπΆ) Β· π΄) = (π΄ Β· ((π D πΉ)βπΆ))) |
55 | 50, 54 | eqtrd 2773 |
. . 3
β’ (π β (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ)) = (π΄ Β· ((π D πΉ)βπΆ))) |
56 | 47, 55 | oveq12d 7379 |
. 2
β’ (π β ((((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) + (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ))) = (0 + (π΄ Β· ((π D πΉ)βπΆ)))) |
57 | 1, 53 | mulcld 11183 |
. . 3
β’ (π β (π΄ Β· ((π D πΉ)βπΆ)) β β) |
58 | 57 | addid2d 11364 |
. 2
β’ (π β (0 + (π΄ Β· ((π D πΉ)βπΆ))) = (π΄ Β· ((π D πΉ)βπΆ))) |
59 | 39, 56, 58 | 3eqtrd 2777 |
1
β’ (π β ((π D ((π Γ {π΄}) βf Β· πΉ))βπΆ) = (π΄ Β· ((π D πΉ)βπΆ))) |