| Step | Hyp | Ref
| Expression |
|---|
| 1 | | dvcmul.a |
. . . 4
β’ (π β π΄ β β) |
| 2 | | fconst6g 6771 |
. . . 4
β’ (π΄ β β β (π Γ {π΄}):πβΆβ) |
| 3 | 1, 2 | syl 17 |
. . 3
β’ (π β (π Γ {π΄}):πβΆβ) |
| 4 | | ssidd 3998 |
. . 3
β’ (π β π β π) |
| 5 | | dvcmul.f |
. . 3
β’ (π β πΉ:πβΆβ) |
| 6 | | dvcmul.x |
. . 3
β’ (π β π β π) |
| 7 | | dvcmul.s |
. . 3
β’ (π β π β {β, β}) |
| 8 | | recnprss 25777 |
. . . . . . . 8
β’ (π β {β, β}
β π β
β) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
| 10 | 9, 5, 6 | dvbss 25774 |
. . . . . 6
β’ (π β dom (π D πΉ) β π) |
| 11 | | dvcmul.c |
. . . . . 6
β’ (π β πΆ β dom (π D πΉ)) |
| 12 | 10, 11 | sseldd 3976 |
. . . . 5
β’ (π β πΆ β π) |
| 13 | 6, 12 | sseldd 3976 |
. . . 4
β’ (π β πΆ β π) |
| 14 | | fconst6g 6771 |
. . . . . . . . 9
β’ (π΄ β β β (β
Γ {π΄}):ββΆβ) |
| 15 | 1, 14 | syl 17 |
. . . . . . . 8
β’ (π β (β Γ {π΄}):ββΆβ) |
| 16 | | ssidd 3998 |
. . . . . . . 8
β’ (π β β β
β) |
| 17 | | dvconst 25790 |
. . . . . . . . . . . 12
β’ (π΄ β β β (β
D (β Γ {π΄})) =
(β Γ {0})) |
| 18 | 1, 17 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β D (β
Γ {π΄})) = (β
Γ {0})) |
| 19 | 18 | dmeqd 5896 |
. . . . . . . . . 10
β’ (π β dom (β D (β
Γ {π΄})) = dom
(β Γ {0})) |
| 20 | | c0ex 11207 |
. . . . . . . . . . . 12
β’ 0 β
V |
| 21 | 20 | fconst 6768 |
. . . . . . . . . . 11
β’ (β
Γ {0}):ββΆ{0} |
| 22 | 21 | fdmi 6720 |
. . . . . . . . . 10
β’ dom
(β Γ {0}) = β |
| 23 | 19, 22 | eqtrdi 2780 |
. . . . . . . . 9
β’ (π β dom (β D (β
Γ {π΄})) =
β) |
| 24 | 9, 23 | sseqtrrd 4016 |
. . . . . . . 8
β’ (π β π β dom (β D (β Γ
{π΄}))) |
| 25 | | dvres3 25786 |
. . . . . . . 8
β’ (((π β {β, β} β§
(β Γ {π΄}):ββΆβ) β§ (β
β β β§ π
β dom (β D (β Γ {π΄})))) β (π D ((β Γ {π΄}) βΎ π)) = ((β D (β Γ {π΄})) βΎ π)) |
| 26 | 7, 15, 16, 24, 25 | syl22anc 836 |
. . . . . . 7
β’ (π β (π D ((β Γ {π΄}) βΎ π)) = ((β D (β Γ {π΄})) βΎ π)) |
| 27 | | xpssres 6009 |
. . . . . . . . 9
β’ (π β β β
((β Γ {π΄})
βΎ π) = (π Γ {π΄})) |
| 28 | 9, 27 | syl 17 |
. . . . . . . 8
β’ (π β ((β Γ {π΄}) βΎ π) = (π Γ {π΄})) |
| 29 | 28 | oveq2d 7418 |
. . . . . . 7
β’ (π β (π D ((β Γ {π΄}) βΎ π)) = (π D (π Γ {π΄}))) |
| 30 | 18 | reseq1d 5971 |
. . . . . . . 8
β’ (π β ((β D (β
Γ {π΄})) βΎ π) = ((β Γ {0})
βΎ π)) |
| 31 | | xpssres 6009 |
. . . . . . . . 9
β’ (π β β β
((β Γ {0}) βΎ π) = (π Γ {0})) |
| 32 | 9, 31 | syl 17 |
. . . . . . . 8
β’ (π β ((β Γ {0})
βΎ π) = (π Γ {0})) |
| 33 | 30, 32 | eqtrd 2764 |
. . . . . . 7
β’ (π β ((β D (β
Γ {π΄})) βΎ π) = (π Γ {0})) |
| 34 | 26, 29, 33 | 3eqtr3d 2772 |
. . . . . 6
β’ (π β (π D (π Γ {π΄})) = (π Γ {0})) |
| 35 | 20 | fconst2 7199 |
. . . . . 6
β’ ((π D (π Γ {π΄})):πβΆ{0} β (π D (π Γ {π΄})) = (π Γ {0})) |
| 36 | 34, 35 | sylibr 233 |
. . . . 5
β’ (π β (π D (π Γ {π΄})):πβΆ{0}) |
| 37 | 36 | fdmd 6719 |
. . . 4
β’ (π β dom (π D (π Γ {π΄})) = π) |
| 38 | 13, 37 | eleqtrrd 2828 |
. . 3
β’ (π β πΆ β dom (π D (π Γ {π΄}))) |
| 39 | 3, 4, 5, 6, 7, 38,
11 | dvmul 25816 |
. 2
β’ (π β ((π D ((π Γ {π΄}) βf Β· πΉ))βπΆ) = ((((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) + (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ)))) |
| 40 | 34 | fveq1d 6884 |
. . . . . 6
β’ (π β ((π D (π Γ {π΄}))βπΆ) = ((π Γ {0})βπΆ)) |
| 41 | 20 | fvconst2 7198 |
. . . . . . 7
β’ (πΆ β π β ((π Γ {0})βπΆ) = 0) |
| 42 | 13, 41 | syl 17 |
. . . . . 6
β’ (π β ((π Γ {0})βπΆ) = 0) |
| 43 | 40, 42 | eqtrd 2764 |
. . . . 5
β’ (π β ((π D (π Γ {π΄}))βπΆ) = 0) |
| 44 | 43 | oveq1d 7417 |
. . . 4
β’ (π β (((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) = (0 Β· (πΉβπΆ))) |
| 45 | 5, 12 | ffvelcdmd 7078 |
. . . . 5
β’ (π β (πΉβπΆ) β β) |
| 46 | 45 | mul02d 11411 |
. . . 4
β’ (π β (0 Β· (πΉβπΆ)) = 0) |
| 47 | 44, 46 | eqtrd 2764 |
. . 3
β’ (π β (((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) = 0) |
| 48 | | fvconst2g 7196 |
. . . . . 6
β’ ((π΄ β β β§ πΆ β π) β ((π Γ {π΄})βπΆ) = π΄) |
| 49 | 1, 13, 48 | syl2anc 583 |
. . . . 5
β’ (π β ((π Γ {π΄})βπΆ) = π΄) |
| 50 | 49 | oveq2d 7418 |
. . . 4
β’ (π β (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ)) = (((π D πΉ)βπΆ) Β· π΄)) |
| 51 | | dvfg 25779 |
. . . . . . 7
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
| 52 | 7, 51 | syl 17 |
. . . . . 6
β’ (π β (π D πΉ):dom (π D πΉ)βΆβ) |
| 53 | 52, 11 | ffvelcdmd 7078 |
. . . . 5
β’ (π β ((π D πΉ)βπΆ) β β) |
| 54 | 53, 1 | mulcomd 11234 |
. . . 4
β’ (π β (((π D πΉ)βπΆ) Β· π΄) = (π΄ Β· ((π D πΉ)βπΆ))) |
| 55 | 50, 54 | eqtrd 2764 |
. . 3
β’ (π β (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ)) = (π΄ Β· ((π D πΉ)βπΆ))) |
| 56 | 47, 55 | oveq12d 7420 |
. 2
β’ (π β ((((π D (π Γ {π΄}))βπΆ) Β· (πΉβπΆ)) + (((π D πΉ)βπΆ) Β· ((π Γ {π΄})βπΆ))) = (0 + (π΄ Β· ((π D πΉ)βπΆ)))) |
| 57 | 1, 53 | mulcld 11233 |
. . 3
β’ (π β (π΄ Β· ((π D πΉ)βπΆ)) β β) |
| 58 | 57 | addlidd 11414 |
. 2
β’ (π β (0 + (π΄ Β· ((π D πΉ)βπΆ))) = (π΄ Β· ((π D πΉ)βπΆ))) |
| 59 | 39, 56, 58 | 3eqtrd 2768 |
1
β’ (π β ((π D ((π Γ {π΄}) βf Β· πΉ))βπΆ) = (π΄ Β· ((π D πΉ)βπΆ))) |
