Step | Hyp | Ref
| Expression |
1 | | mplmon.s |
. . 3
β’ π = (πΌ mPoly π
) |
2 | | mplmon.b |
. . 3
β’ π΅ = (Baseβπ) |
3 | | eqid 2737 |
. . 3
β’
(.rβπ
) = (.rβπ
) |
4 | | mplmonmul.t |
. . 3
β’ Β· =
(.rβπ) |
5 | | mplmon.d |
. . 3
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
6 | | mplmon.z |
. . . 4
β’ 0 =
(0gβπ
) |
7 | | mplmon.o |
. . . 4
β’ 1 =
(1rβπ
) |
8 | | mplmon.i |
. . . 4
β’ (π β πΌ β π) |
9 | | mplmon.r |
. . . 4
β’ (π β π
β Ring) |
10 | | mplmon.x |
. . . 4
β’ (π β π β π·) |
11 | 1, 2, 6, 7, 5, 8, 9, 10 | mplmon 21452 |
. . 3
β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) β π΅) |
12 | | mplmonmul.x |
. . . 4
β’ (π β π β π·) |
13 | 1, 2, 6, 7, 5, 8, 9, 12 | mplmon 21452 |
. . 3
β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) β π΅) |
14 | 1, 2, 3, 4, 5, 11,
13 | mplmul 21431 |
. 2
β’ (π β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 )) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) = (π β π· β¦ (π
Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))))))) |
15 | | eqeq1 2741 |
. . . . 5
β’ (π¦ = π β (π¦ = (π βf + π) β π = (π βf + π))) |
16 | 15 | ifbid 4514 |
. . . 4
β’ (π¦ = π β if(π¦ = (π βf + π), 1 , 0 ) = if(π = (π βf + π), 1 , 0 )) |
17 | 16 | cbvmptv 5223 |
. . 3
β’ (π¦ β π· β¦ if(π¦ = (π βf + π), 1 , 0 )) = (π β π· β¦ if(π = (π βf + π), 1 , 0 )) |
18 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π β {π₯ β π· β£ π₯ βr β€ π}) |
19 | 18 | snssd 4774 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β {π} β {π₯ β π· β£ π₯ βr β€ π}) |
20 | 19 | resmptd 5999 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π}) = (π β {π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))))) |
21 | 20 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π
Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π})) = (π
Ξ£g (π β {π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))))) |
22 | 9 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π
β Ring) |
23 | | ringmnd 19981 |
. . . . . . . . 9
β’ (π
β Ring β π
β Mnd) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π
β Mnd) |
25 | 10 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π β π·) |
26 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π¦ = π β if(π¦ = π, 1 , 0 ) = 1 ) |
27 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) = (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) |
28 | 7 | fvexi 6861 |
. . . . . . . . . . . . 13
β’ 1 β
V |
29 | 26, 27, 28 | fvmpt 6953 |
. . . . . . . . . . . 12
β’ (π β π· β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) = 1 ) |
30 | 25, 29 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) = 1 ) |
31 | | ssrab2 4042 |
. . . . . . . . . . . . 13
β’ {π₯ β π· β£ π₯ βr β€ π} β π· |
32 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π β π·) |
33 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ {π₯ β π· β£ π₯ βr β€ π} = {π₯ β π· β£ π₯ βr β€ π} |
34 | 5, 33 | psrbagconcl 21352 |
. . . . . . . . . . . . . 14
β’ ((π β π· β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) β {π₯ β π· β£ π₯ βr β€ π}) |
35 | 32, 18, 34 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) β {π₯ β π· β£ π₯ βr β€ π}) |
36 | 31, 35 | sselid 3947 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) β π·) |
37 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π βf β π) β (π¦ = π β (π βf β π) = π)) |
38 | 37 | ifbid 4514 |
. . . . . . . . . . . . 13
β’ (π¦ = (π βf β π) β if(π¦ = π, 1 , 0 ) = if((π βf β π) = π, 1 , 0 )) |
39 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) = (π¦ β π· β¦ if(π¦ = π, 1 , 0 )) |
40 | 6 | fvexi 6861 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
41 | 28, 40 | ifex 4541 |
. . . . . . . . . . . . 13
β’ if((π βf β
π) = π, 1 , 0 ) β
V |
42 | 38, 39, 41 | fvmpt 6953 |
. . . . . . . . . . . 12
β’ ((π βf β
π) β π· β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)) = if((π βf β
π) = π, 1 , 0 )) |
43 | 36, 42 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)) = if((π βf β
π) = π, 1 , 0 )) |
44 | 30, 43 | oveq12d 7380 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = ( 1 (.rβπ
)if((π βf β π) = π, 1 , 0 ))) |
45 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(Baseβπ
) =
(Baseβπ
) |
46 | 45, 7 | ringidcl 19996 |
. . . . . . . . . . . . 13
β’ (π
β Ring β 1 β
(Baseβπ
)) |
47 | 45, 6 | ring0cl 19997 |
. . . . . . . . . . . . 13
β’ (π
β Ring β 0 β
(Baseβπ
)) |
48 | 46, 47 | ifcld 4537 |
. . . . . . . . . . . 12
β’ (π
β Ring β if((π βf β
π) = π, 1 , 0 ) β (Baseβπ
)) |
49 | 22, 48 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β if((π βf β π) = π, 1 , 0 ) β (Baseβπ
)) |
50 | 45, 3, 7 | ringlidm 19999 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ if((π βf β
π) = π, 1 , 0 ) β (Baseβπ
)) β ( 1 (.rβπ
)if((π βf β π) = π, 1 , 0 )) = if((π βf β
π) = π, 1 , 0 )) |
51 | 22, 49, 50 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ( 1 (.rβπ
)if((π βf β π) = π, 1 , 0 )) = if((π βf β
π) = π, 1 , 0 )) |
52 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π· β π:πΌβΆβ0) |
53 | 32, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π:πΌβΆβ0) |
54 | 53 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
55 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π·) β π β π·) |
56 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π· β π:πΌβΆβ0) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β π:πΌβΆβ0) |
58 | 57 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π§ β πΌ) β (πβπ§) β
β0) |
59 | 58 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
60 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π· β π:πΌβΆβ0) |
61 | 12, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π:πΌβΆβ0) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π·) β π:πΌβΆβ0) |
63 | 62 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π§ β πΌ) β (πβπ§) β
β0) |
64 | 63 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
65 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
66 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
67 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
68 | | subadd 11411 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ§) β β β§ (πβπ§) β β β§ (πβπ§) β β) β (((πβπ§) β (πβπ§)) = (πβπ§) β ((πβπ§) + (πβπ§)) = (πβπ§))) |
69 | 65, 66, 67, 68 | syl3an 1161 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ§) β β0 β§ (πβπ§) β β0 β§ (πβπ§) β β0) β (((πβπ§) β (πβπ§)) = (πβπ§) β ((πβπ§) + (πβπ§)) = (πβπ§))) |
70 | 54, 59, 64, 69 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β§ π§ β πΌ) β (((πβπ§) β (πβπ§)) = (πβπ§) β ((πβπ§) + (πβπ§)) = (πβπ§))) |
71 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
β’ (((πβπ§) + (πβπ§)) = (πβπ§) β (πβπ§) = ((πβπ§) + (πβπ§))) |
72 | 70, 71 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β§ π§ β πΌ) β (((πβπ§) β (πβπ§)) = (πβπ§) β (πβπ§) = ((πβπ§) + (πβπ§)))) |
73 | 72 | ralbidva 3173 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (βπ§ β πΌ ((πβπ§) β (πβπ§)) = (πβπ§) β βπ§ β πΌ (πβπ§) = ((πβπ§) + (πβπ§)))) |
74 | | mpteqb 6972 |
. . . . . . . . . . . . . 14
β’
(βπ§ β
πΌ ((πβπ§) β (πβπ§)) β V β ((π§ β πΌ β¦ ((πβπ§) β (πβπ§))) = (π§ β πΌ β¦ (πβπ§)) β βπ§ β πΌ ((πβπ§) β (πβπ§)) = (πβπ§))) |
75 | | ovexd 7397 |
. . . . . . . . . . . . . 14
β’ (π§ β πΌ β ((πβπ§) β (πβπ§)) β V) |
76 | 74, 75 | mprg 3071 |
. . . . . . . . . . . . 13
β’ ((π§ β πΌ β¦ ((πβπ§) β (πβπ§))) = (π§ β πΌ β¦ (πβπ§)) β βπ§ β πΌ ((πβπ§) β (πβπ§)) = (πβπ§)) |
77 | | mpteqb 6972 |
. . . . . . . . . . . . . 14
β’
(βπ§ β
πΌ (πβπ§) β V β ((π§ β πΌ β¦ (πβπ§)) = (π§ β πΌ β¦ ((πβπ§) + (πβπ§))) β βπ§ β πΌ (πβπ§) = ((πβπ§) + (πβπ§)))) |
78 | | fvexd 6862 |
. . . . . . . . . . . . . 14
β’ (π§ β πΌ β (πβπ§) β V) |
79 | 77, 78 | mprg 3071 |
. . . . . . . . . . . . 13
β’ ((π§ β πΌ β¦ (πβπ§)) = (π§ β πΌ β¦ ((πβπ§) + (πβπ§))) β βπ§ β πΌ (πβπ§) = ((πβπ§) + (πβπ§))) |
80 | 73, 76, 79 | 3bitr4g 314 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π§ β πΌ β¦ ((πβπ§) β (πβπ§))) = (π§ β πΌ β¦ (πβπ§)) β (π§ β πΌ β¦ (πβπ§)) = (π§ β πΌ β¦ ((πβπ§) + (πβπ§))))) |
81 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β πΌ β π) |
82 | 53 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
83 | 57 | feqmptd 6915 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β π = (π§ β πΌ β¦ (πβπ§))) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
85 | 81, 54, 59, 82, 84 | offval2 7642 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) = (π§ β πΌ β¦ ((πβπ§) β (πβπ§)))) |
86 | 62 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β π = (π§ β πΌ β¦ (πβπ§))) |
87 | 86 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
88 | 85, 87 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π βf β π) = π β (π§ β πΌ β¦ ((πβπ§) β (πβπ§))) = (π§ β πΌ β¦ (πβπ§)))) |
89 | 8 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β πΌ β π) |
90 | 89, 58, 63, 83, 86 | offval2 7642 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π·) β (π βf + π) = (π§ β πΌ β¦ ((πβπ§) + (πβπ§)))) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf + π) = (π§ β πΌ β¦ ((πβπ§) + (πβπ§)))) |
92 | 82, 91 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π = (π βf + π) β (π§ β πΌ β¦ (πβπ§)) = (π§ β πΌ β¦ ((πβπ§) + (πβπ§))))) |
93 | 80, 88, 92 | 3bitr4d 311 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π βf β π) = π β π = (π βf + π))) |
94 | 93 | ifbid 4514 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β if((π βf β π) = π, 1 , 0 ) = if(π = (π βf + π), 1 , 0 )) |
95 | 44, 51, 94 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = if(π = (π βf + π), 1 , 0 )) |
96 | 94, 49 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β if(π = (π βf + π), 1 , 0 ) β (Baseβπ
)) |
97 | 95, 96 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) β
(Baseβπ
)) |
98 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) = ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)) |
99 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π β (π βf β π) = (π βf β π)) |
100 | 99 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)) = ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) |
101 | 98, 100 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) |
102 | 45, 101 | gsumsn 19738 |
. . . . . . . 8
β’ ((π
β Mnd β§ π β π· β§ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) β
(Baseβπ
)) β
(π
Ξ£g (π β {π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))))) = (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) |
103 | 24, 25, 97, 102 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π
Ξ£g (π β {π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))))) = (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) |
104 | 21, 103, 95 | 3eqtrd 2781 |
. . . . . 6
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π
Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π})) = if(π = (π βf + π), 1 , 0 )) |
105 | 6 | gsum0 18546 |
. . . . . . 7
β’ (π
Ξ£g
β
) = 0 |
106 | | disjsn 4677 |
. . . . . . . . 9
β’ (({π₯ β π· β£ π₯ βr β€ π} β© {π}) = β
β Β¬ π β {π₯ β π· β£ π₯ βr β€ π}) |
107 | 9 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π
β Ring) |
108 | 1, 45, 2, 5, 11 | mplelf 21420 |
. . . . . . . . . . . . . . 15
β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )):π·βΆ(Baseβπ
)) |
109 | 108 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )):π·βΆ(Baseβπ
)) |
110 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π β {π₯ β π· β£ π₯ βr β€ π}) |
111 | 31, 110 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π β π·) |
112 | 109, 111 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) β (Baseβπ
)) |
113 | 1, 45, 2, 5, 13 | mplelf 21420 |
. . . . . . . . . . . . . . 15
β’ (π β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )):π·βΆ(Baseβπ
)) |
114 | 113 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )):π·βΆ(Baseβπ
)) |
115 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β π β π·) |
116 | 5, 33 | psrbagconcl 21352 |
. . . . . . . . . . . . . . . 16
β’ ((π β π· β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) β {π₯ β π· β£ π₯ βr β€ π}) |
117 | 115, 110,
116 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) β {π₯ β π· β£ π₯ βr β€ π}) |
118 | 31, 117 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (π βf β π) β π·) |
119 | 114, 118 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)) β
(Baseβπ
)) |
120 | 45, 3 | ringcl 19988 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) β (Baseβπ
) β§ ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)) β
(Baseβπ
)) β
(((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) β
(Baseβπ
)) |
121 | 107, 112,
119, 120 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) β
(Baseβπ
)) |
122 | 121 | fmpttd 7068 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))):{π₯ β π· β£ π₯ βr β€ π}βΆ(Baseβπ
)) |
123 | | ffn 6673 |
. . . . . . . . . . 11
β’ ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))):{π₯ β π· β£ π₯ βr β€ π}βΆ(Baseβπ
) β (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) Fn {π₯ β π· β£ π₯ βr β€ π}) |
124 | | fnresdisj 6626 |
. . . . . . . . . . 11
β’ ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) Fn {π₯ β π· β£ π₯ βr β€ π} β (({π₯ β π· β£ π₯ βr β€ π} β© {π}) = β
β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π}) = β
)) |
125 | 122, 123,
124 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (({π₯ β π· β£ π₯ βr β€ π} β© {π}) = β
β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π}) = β
)) |
126 | 125 | biimpa 478 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ ({π₯ β π· β£ π₯ βr β€ π} β© {π}) = β
) β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π}) = β
) |
127 | 106, 126 | sylan2br 596 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ Β¬ π β {π₯ β π· β£ π₯ βr β€ π}) β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π}) = β
) |
128 | 127 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ π β π·) β§ Β¬ π β {π₯ β π· β£ π₯ βr β€ π}) β (π
Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π})) = (π
Ξ£g
β
)) |
129 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ βr β€ (π βf + π) β π βr β€ (π βf + π))) |
130 | 58 | nn0red 12481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π§ β πΌ) β (πβπ§) β β) |
131 | | nn0addge1 12466 |
. . . . . . . . . . . . . 14
β’ (((πβπ§) β β β§ (πβπ§) β β0) β (πβπ§) β€ ((πβπ§) + (πβπ§))) |
132 | 130, 63, 131 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π§ β πΌ) β (πβπ§) β€ ((πβπ§) + (πβπ§))) |
133 | 132 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β βπ§ β πΌ (πβπ§) β€ ((πβπ§) + (πβπ§))) |
134 | | ovexd 7397 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π§ β πΌ) β ((πβπ§) + (πβπ§)) β V) |
135 | 89, 58, 134, 83, 90 | ofrfval2 7643 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β (π βr β€ (π βf + π) β βπ§ β πΌ (πβπ§) β€ ((πβπ§) + (πβπ§)))) |
136 | 133, 135 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β π βr β€ (π βf + π)) |
137 | 129, 55, 136 | elrabd 3652 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β π β {π₯ β π· β£ π₯ βr β€ (π βf + π)}) |
138 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π = (π βf + π) β (π₯ βr β€ π β π₯ βr β€ (π βf + π))) |
139 | 138 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π = (π βf + π) β {π₯ β π· β£ π₯ βr β€ π} = {π₯ β π· β£ π₯ βr β€ (π βf + π)}) |
140 | 139 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = (π βf + π) β (π β {π₯ β π· β£ π₯ βr β€ π} β π β {π₯ β π· β£ π₯ βr β€ (π βf + π)})) |
141 | 137, 140 | syl5ibrcom 247 |
. . . . . . . . 9
β’ ((π β§ π β π·) β (π = (π βf + π) β π β {π₯ β π· β£ π₯ βr β€ π})) |
142 | 141 | con3dimp 410 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ Β¬ π β {π₯ β π· β£ π₯ βr β€ π}) β Β¬ π = (π βf + π)) |
143 | 142 | iffalsed 4502 |
. . . . . . 7
β’ (((π β§ π β π·) β§ Β¬ π β {π₯ β π· β£ π₯ βr β€ π}) β if(π = (π βf + π), 1 , 0 ) = 0 ) |
144 | 105, 128,
143 | 3eqtr4a 2803 |
. . . . . 6
β’ (((π β§ π β π·) β§ Β¬ π β {π₯ β π· β£ π₯ βr β€ π}) β (π
Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π})) = if(π = (π βf + π), 1 , 0 )) |
145 | 104, 144 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π β π·) β (π
Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π})) = if(π = (π βf + π), 1 , 0 )) |
146 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π·) β π
β Ring) |
147 | | ringcmn 20010 |
. . . . . . 7
β’ (π
β Ring β π
β CMnd) |
148 | 146, 147 | syl 17 |
. . . . . 6
β’ ((π β§ π β π·) β π
β CMnd) |
149 | 5 | psrbaglefi 21350 |
. . . . . . 7
β’ (π β π· β {π₯ β π· β£ π₯ βr β€ π} β Fin) |
150 | 149 | adantl 483 |
. . . . . 6
β’ ((π β§ π β π·) β {π₯ β π· β£ π₯ βr β€ π} β Fin) |
151 | | ssdif 4104 |
. . . . . . . . . . . 12
β’ ({π₯ β π· β£ π₯ βr β€ π} β π· β ({π₯ β π· β£ π₯ βr β€ π} β {π}) β (π· β {π})) |
152 | 31, 151 | ax-mp 5 |
. . . . . . . . . . 11
β’ ({π₯ β π· β£ π₯ βr β€ π} β {π}) β (π· β {π}) |
153 | 152 | sseli 3945 |
. . . . . . . . . 10
β’ (π β ({π₯ β π· β£ π₯ βr β€ π} β {π}) β π β (π· β {π})) |
154 | 108 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (π¦ β π· β¦ if(π¦ = π, 1 , 0 )):π·βΆ(Baseβπ
)) |
155 | | eldifsni 4755 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π· β {π}) β π¦ β π) |
156 | 155 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π¦ β (π· β {π})) β π¦ β π) |
157 | 156 | neneqd 2949 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π¦ β (π· β {π})) β Β¬ π¦ = π) |
158 | 157 | iffalsed 4502 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π¦ β (π· β {π})) β if(π¦ = π, 1 , 0 ) = 0 ) |
159 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’
(β0 βm πΌ) β V |
160 | 5, 159 | rabex2 5296 |
. . . . . . . . . . . . 13
β’ π· β V |
161 | 160 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β π· β V) |
162 | 158, 161 | suppss2 8136 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 )) supp 0 ) β {π}) |
163 | 40 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β 0 β V) |
164 | 154, 162,
161, 163 | suppssr 8132 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π β (π· β {π})) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) = 0 ) |
165 | 153, 164 | sylan2 594 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π β ({π₯ β π· β£ π₯ βr β€ π} β {π})) β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ) = 0 ) |
166 | 165 | oveq1d 7377 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β ({π₯ β π· β£ π₯ βr β€ π} β {π})) β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = ( 0 (.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) |
167 | | eldifi 4091 |
. . . . . . . . 9
β’ (π β ({π₯ β π· β£ π₯ βr β€ π} β {π}) β π β {π₯ β π· β£ π₯ βr β€ π}) |
168 | 45, 3, 6 | ringlz 20018 |
. . . . . . . . . 10
β’ ((π
β Ring β§ ((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)) β
(Baseβπ
)) β (
0
(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = 0 ) |
169 | 107, 119,
168 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π β {π₯ β π· β£ π₯ βr β€ π}) β ( 0 (.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = 0 ) |
170 | 167, 169 | sylan2 594 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β ({π₯ β π· β£ π₯ βr β€ π} β {π})) β ( 0 (.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = 0 ) |
171 | 166, 170 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π β ({π₯ β π· β£ π₯ βr β€ π} β {π})) β (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))) = 0 ) |
172 | 160 | rabex 5294 |
. . . . . . . 8
β’ {π₯ β π· β£ π₯ βr β€ π} β V |
173 | 172 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π·) β {π₯ β π· β£ π₯ βr β€ π} β V) |
174 | 171, 173 | suppss2 8136 |
. . . . . 6
β’ ((π β§ π β π·) β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) supp 0 ) β
{π}) |
175 | 160 | mptrabex 7180 |
. . . . . . . . 9
β’ (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β
V |
176 | | funmpt 6544 |
. . . . . . . . 9
β’ Fun
(π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) |
177 | 175, 176,
40 | 3pm3.2i 1340 |
. . . . . . . 8
β’ ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β V β§ Fun
(π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β§ 0 β
V) |
178 | 177 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π·) β ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β V β§ Fun
(π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β§ 0 β
V)) |
179 | | snfi 8995 |
. . . . . . . 8
β’ {π} β Fin |
180 | 179 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π·) β {π} β Fin) |
181 | | suppssfifsupp 9327 |
. . . . . . 7
β’ ((((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β V β§ Fun
(π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) β§ 0 β V)
β§ ({π} β Fin β§
((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) supp 0 ) β
{π})) β (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) finSupp 0
) |
182 | 178, 180,
174, 181 | syl12anc 836 |
. . . . . 6
β’ ((π β§ π β π·) β (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) finSupp 0
) |
183 | 45, 6, 148, 150, 122, 174, 182 | gsumres 19697 |
. . . . 5
β’ ((π β§ π β π·) β (π
Ξ£g ((π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))) βΎ {π})) = (π
Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))))) |
184 | 145, 183 | eqtr3d 2779 |
. . . 4
β’ ((π β§ π β π·) β if(π = (π βf + π), 1 , 0 ) = (π
Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π)))))) |
185 | 184 | mpteq2dva 5210 |
. . 3
β’ (π β (π β π· β¦ if(π = (π βf + π), 1 , 0 )) = (π β π· β¦ (π
Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))))))) |
186 | 17, 185 | eqtrid 2789 |
. 2
β’ (π β (π¦ β π· β¦ if(π¦ = (π βf + π), 1 , 0 )) = (π β π· β¦ (π
Ξ£g (π β {π₯ β π· β£ π₯ βr β€ π} β¦ (((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))βπ)(.rβπ
)((π¦ β π· β¦ if(π¦ = π, 1 , 0 ))β(π βf β
π))))))) |
187 | 14, 186 | eqtr4d 2780 |
1
β’ (π β ((π¦ β π· β¦ if(π¦ = π, 1 , 0 )) Β· (π¦ β π· β¦ if(π¦ = π, 1 , 0 ))) = (π¦ β π· β¦ if(π¦ = (π βf + π), 1 , 0 ))) |