Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . 3
β’ (πΌ mPwSer π
) = (πΌ mPwSer π
) |
2 | | eqid 2726 |
. . 3
β’
(Baseβ(πΌ
mPwSer π
)) =
(Baseβ(πΌ mPwSer π
)) |
3 | | psdmplcl.i |
. . 3
β’ (π β πΌ β π) |
4 | | psdmplcl.r |
. . . 4
β’ (π β π
β Mnd) |
5 | | mndmgm 18672 |
. . . 4
β’ (π
β Mnd β π
β Mgm) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β π
β Mgm) |
7 | | psdmplcl.x |
. . 3
β’ (π β π β πΌ) |
8 | | psdmplcl.p |
. . . . 5
β’ π = (πΌ mPoly π
) |
9 | | psdmplcl.b |
. . . . 5
β’ π΅ = (Baseβπ) |
10 | 8, 1, 9, 2 | mplbasss 21894 |
. . . 4
β’ π΅ β (Baseβ(πΌ mPwSer π
)) |
11 | | psdmplcl.f |
. . . 4
β’ (π β πΉ β π΅) |
12 | 10, 11 | sselid 3975 |
. . 3
β’ (π β πΉ β (Baseβ(πΌ mPwSer π
))) |
13 | 1, 2, 3, 6, 7, 12 | psdcl 22040 |
. 2
β’ (π β (((πΌ mPSDer π
)βπ)βπΉ) β (Baseβ(πΌ mPwSer π
))) |
14 | | eqid 2726 |
. . . 4
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
15 | 1, 2, 14, 3, 6, 7,
12 | psdval 22038 |
. . 3
β’ (π β (((πΌ mPSDer π
)βπ)βπΉ) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))))) |
16 | | ovex 7437 |
. . . . . . 7
β’
(β0 βm πΌ) β V |
17 | 16 | rabex 5325 |
. . . . . 6
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β
V |
18 | 17 | a1i 11 |
. . . . 5
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β
V) |
19 | 18 | mptexd 7220 |
. . . 4
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) β V) |
20 | | fvexd 6899 |
. . . 4
β’ (π β (0gβπ
) β V) |
21 | | funmpt 6579 |
. . . . 5
β’ Fun
(π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) |
22 | 21 | a1i 11 |
. . . 4
β’ (π β Fun (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))))) |
23 | | simpr 484 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
24 | 14 | psrbagsn 21962 |
. . . . . . . . . . 11
β’ (πΌ β π β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
25 | 3, 24 | syl 17 |
. . . . . . . . . 10
β’ (π β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
26 | 25 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
27 | 14 | psrbagaddcl 21818 |
. . . . . . . . 9
β’ ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β§ (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
28 | 23, 26, 27 | syl2anc 583 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
29 | | eqidd 2727 |
. . . . . . . 8
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) |
30 | | eqid 2726 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
31 | 8, 30, 9, 14, 11 | mplelf 21895 |
. . . . . . . . 9
β’ (π β πΉ:{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}βΆ(Baseβπ
)) |
32 | 31 | feqmptd 6953 |
. . . . . . . 8
β’ (π β πΉ = (π§ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβπ§))) |
33 | | fveq2 6884 |
. . . . . . . 8
β’ (π§ = (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β (πΉβπ§) = (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) |
34 | 28, 29, 32, 33 | fmptco 7122 |
. . . . . . 7
β’ (π β (πΉ β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) |
35 | | eqid 2726 |
. . . . . . . . 9
β’
(0gβπ
) = (0gβπ
) |
36 | 8, 9, 35, 11, 4 | mplelsfi 21892 |
. . . . . . . 8
β’ (π β πΉ finSupp (0gβπ
)) |
37 | 28 | fmpttd 7109 |
. . . . . . . . 9
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆ{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
38 | | ovex 7437 |
. . . . . . . . . . . . . . 15
β’ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β V |
39 | | eqid 2726 |
. . . . . . . . . . . . . . 15
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
40 | 38, 39 | fnmpti 6686 |
. . . . . . . . . . . . . 14
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) Fn {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) Fn {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
42 | | dffn3 6723 |
. . . . . . . . . . . . 13
β’ ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) Fn {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆran
(π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) |
43 | 41, 42 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆran
(π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) |
44 | 43, 37 | fcod 6736 |
. . . . . . . . . . 11
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆran
(π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) |
45 | 44 | ffnd 6711 |
. . . . . . . . . 10
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) Fn {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
46 | | fnresi 6672 |
. . . . . . . . . . 11
β’ ( I
βΎ {β β
(β0 βm πΌ) β£ (β‘β β β) β Fin}) Fn {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
47 | 46 | a1i 11 |
. . . . . . . . . 10
β’ (π β ( I βΎ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) Fn {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
48 | 14 | psrbagf 21808 |
. . . . . . . . . . . . . . . . 17
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π:πΌβΆβ0) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π:πΌβΆβ0) |
50 | 49 | ffvelcdmda 7079 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (πβπ) β
β0) |
51 | 50 | nn0cnd 12535 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (πβπ) β β) |
52 | | ax-1cn 11167 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
53 | | 0cn 11207 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
54 | 52, 53 | ifcli 4570 |
. . . . . . . . . . . . . . 15
β’ if(π = π, 1, 0) β β |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β if(π = π, 1, 0) β β) |
56 | 51, 55 | pncand 11573 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (((πβπ) + if(π = π, 1, 0)) β if(π = π, 1, 0)) = (πβπ)) |
57 | 56 | mpteq2dva 5241 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β πΌ β¦ (((πβπ) + if(π = π, 1, 0)) β if(π = π, 1, 0))) = (π β πΌ β¦ (πβπ))) |
58 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
59 | 25 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
60 | 14 | psrbagaddcl 21818 |
. . . . . . . . . . . . . . 15
β’ ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β§ (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
61 | 58, 59, 60 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
62 | 14 | psrbagf 21808 |
. . . . . . . . . . . . . . 15
β’ ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))):πΌβΆβ0) |
63 | 62 | ffnd 6711 |
. . . . . . . . . . . . . 14
β’ ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) Fn πΌ) |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) Fn πΌ) |
65 | | 1ex 11211 |
. . . . . . . . . . . . . . . 16
β’ 1 β
V |
66 | | c0ex 11209 |
. . . . . . . . . . . . . . . 16
β’ 0 β
V |
67 | 65, 66 | ifex 4573 |
. . . . . . . . . . . . . . 15
β’ if(π¦ = π, 1, 0) β V |
68 | | eqid 2726 |
. . . . . . . . . . . . . . 15
β’ (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) = (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) |
69 | 67, 68 | fnmpti 6686 |
. . . . . . . . . . . . . 14
β’ (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) Fn πΌ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)) Fn πΌ) |
71 | 3 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β πΌ β π) |
72 | | inidm 4213 |
. . . . . . . . . . . . 13
β’ (πΌ β© πΌ) = πΌ |
73 | 48 | ffnd 6711 |
. . . . . . . . . . . . . . 15
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π Fn πΌ) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π Fn πΌ) |
75 | | eqidd 2727 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β (πβπ) = (πβπ)) |
76 | | eqeq1 2730 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π¦ = π β π = π)) |
77 | 76 | ifbid 4546 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β if(π¦ = π, 1, 0) = if(π = π, 1, 0)) |
78 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β π β πΌ) |
79 | 65, 66 | ifex 4573 |
. . . . . . . . . . . . . . . 16
β’ if(π = π, 1, 0) β V |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β if(π = π, 1, 0) β V) |
81 | 68, 77, 78, 80 | fvmptd3 7014 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β ((π¦ β πΌ β¦ if(π¦ = π, 1, 0))βπ) = if(π = π, 1, 0)) |
82 | 74, 70, 71, 71, 72, 75, 81 | ofval 7677 |
. . . . . . . . . . . . 13
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β πΌ) β ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))βπ) = ((πβπ) + if(π = π, 1, 0))) |
83 | 64, 70, 71, 71, 72, 82, 81 | offval 7675 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) = (π β πΌ β¦ (((πβπ) + if(π = π, 1, 0)) β if(π = π, 1, 0)))) |
84 | 49 | feqmptd 6953 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π = (π β πΌ β¦ (πβπ))) |
85 | 57, 83, 84 | 3eqtr4d 2776 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) = π) |
86 | 28 | adantlr 712 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
87 | 86 | fmpttd 7109 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆ{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
88 | 87, 58 | fvco3d 6984 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))βπ) = ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))β((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))βπ))) |
89 | | eqid 2726 |
. . . . . . . . . . . . . 14
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) = (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
90 | | oveq1 7411 |
. . . . . . . . . . . . . 14
β’ (π = π β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) = (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
91 | | ovexd 7439 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β V) |
92 | 89, 90, 58, 91 | fvmptd3 7014 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))βπ) = (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
93 | 92 | fveq2d 6888 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))β((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))βπ)) = ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))β(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) |
94 | | oveq1 7411 |
. . . . . . . . . . . . 13
β’ (π = (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β (π βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) = ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
95 | | ovexd 7439 |
. . . . . . . . . . . . 13
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) β V) |
96 | 39, 94, 61, 95 | fvmptd3 7014 |
. . . . . . . . . . . 12
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0))))β(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) = ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
97 | 88, 93, 96 | 3eqtrd 2770 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))βπ) = ((π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))) βf β (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) |
98 | | fvresi 7166 |
. . . . . . . . . . . 12
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β (( I
βΎ {β β
(β0 βm πΌ) β£ (β‘β β β) β Fin})βπ) = π) |
99 | 98 | adantl 481 |
. . . . . . . . . . 11
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (( I
βΎ {β β
(β0 βm πΌ) β£ (β‘β β β) β Fin})βπ) = π) |
100 | 85, 97, 99 | 3eqtr4d 2776 |
. . . . . . . . . 10
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))βπ) = (( I βΎ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin})βπ)) |
101 | 45, 47, 100 | eqfnfvd 7028 |
. . . . . . . . 9
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) = ( I βΎ {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin})) |
102 | | fcof1 7280 |
. . . . . . . . 9
β’ (((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}βΆ{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β§ ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf β
(π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) = ( I βΎ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin})) β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}β1-1β{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
103 | 37, 101, 102 | syl2anc 583 |
. . . . . . . 8
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))):{β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}β1-1β{β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
104 | 36, 103, 20, 11 | fsuppco 9396 |
. . . . . . 7
β’ (π β (πΉ β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) finSupp
(0gβπ
)) |
105 | 34, 104 | eqbrtrrd 5165 |
. . . . . 6
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) finSupp
(0gβπ
)) |
106 | 105 | fsuppimpd 9368 |
. . . . 5
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) supp (0gβπ
)) β Fin) |
107 | | ssidd 4000 |
. . . . . 6
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) supp (0gβπ
)) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) supp (0gβπ
))) |
108 | | eqid 2726 |
. . . . . . . 8
β’
(.gβπ
) = (.gβπ
) |
109 | 30, 108, 35 | mulgnn0z 19026 |
. . . . . . 7
β’ ((π
β Mnd β§ π β β0)
β (π(.gβπ
)(0gβπ
)) = (0gβπ
)) |
110 | 4, 109 | sylan 579 |
. . . . . 6
β’ ((π β§ π β β0) β (π(.gβπ
)(0gβπ
)) = (0gβπ
)) |
111 | 14 | psrbagf 21808 |
. . . . . . . . 9
β’ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β π:πΌβΆβ0) |
112 | 111 | adantl 481 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π:πΌβΆβ0) |
113 | 7 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β π β πΌ) |
114 | 112, 113 | ffvelcdmd 7080 |
. . . . . . 7
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (πβπ) β
β0) |
115 | | peano2nn0 12513 |
. . . . . . 7
β’ ((πβπ) β β0 β ((πβπ) + 1) β
β0) |
116 | 114, 115 | syl 17 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β ((πβπ) + 1) β
β0) |
117 | | fvexd 6899 |
. . . . . 6
β’ ((π β§ π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin}) β (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))) β V) |
118 | 107, 110,
116, 117, 20 | suppssov2 8181 |
. . . . 5
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) supp (0gβπ
)) β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))) supp (0gβπ
))) |
119 | 106, 118 | ssfid 9266 |
. . . 4
β’ (π β ((π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) supp (0gβπ
)) β Fin) |
120 | 19, 20, 22, 119 | isfsuppd 9365 |
. . 3
β’ (π β (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (((πβπ) + 1)(.gβπ
)(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) finSupp
(0gβπ
)) |
121 | 15, 120 | eqbrtrd 5163 |
. 2
β’ (π β (((πΌ mPSDer π
)βπ)βπΉ) finSupp (0gβπ
)) |
122 | 8, 1, 2, 35, 9 | mplelbas 21888 |
. 2
β’ ((((πΌ mPSDer π
)βπ)βπΉ) β π΅ β ((((πΌ mPSDer π
)βπ)βπΉ) β (Baseβ(πΌ mPwSer π
)) β§ (((πΌ mPSDer π
)βπ)βπΉ) finSupp (0gβπ
))) |
123 | 13, 121, 122 | sylanbrc 582 |
1
β’ (π β (((πΌ mPSDer π
)βπ)βπΉ) β π΅) |