Step | Hyp | Ref
| Expression |
1 | | hashreprin.1 |
. . . . 5
β’ (π β π΅ β β) |
2 | | reprval.m |
. . . . 5
β’ (π β π β β€) |
3 | | reprval.s |
. . . . 5
β’ (π β π β
β0) |
4 | | hashreprin.b |
. . . . 5
β’ (π β π΅ β Fin) |
5 | 1, 2, 3, 4 | reprfi 33617 |
. . . 4
β’ (π β (π΅(reprβπ)π) β Fin) |
6 | | inss2 4229 |
. . . . . 6
β’ (π΄ β© π΅) β π΅ |
7 | 6 | a1i 11 |
. . . . 5
β’ (π β (π΄ β© π΅) β π΅) |
8 | 1, 2, 3, 7 | reprss 33618 |
. . . 4
β’ (π β ((π΄ β© π΅)(reprβπ)π) β (π΅(reprβπ)π)) |
9 | 5, 8 | ssfid 9264 |
. . 3
β’ (π β ((π΄ β© π΅)(reprβπ)π) β Fin) |
10 | | 1cnd 11206 |
. . 3
β’ (π β 1 β
β) |
11 | | fsumconst 15733 |
. . 3
β’ ((((π΄ β© π΅)(reprβπ)π) β Fin β§ 1 β β) β
Ξ£π β ((π΄ β© π΅)(reprβπ)π)1 = ((β―β((π΄ β© π΅)(reprβπ)π)) Β· 1)) |
12 | 9, 10, 11 | syl2anc 585 |
. 2
β’ (π β Ξ£π β ((π΄ β© π΅)(reprβπ)π)1 = ((β―β((π΄ β© π΅)(reprβπ)π)) Β· 1)) |
13 | 10 | ralrimivw 3151 |
. . . 4
β’ (π β βπ β ((π΄ β© π΅)(reprβπ)π)1 β β) |
14 | 5 | olcd 873 |
. . . 4
β’ (π β ((π΅(reprβπ)π) β (β€β₯β0)
β¨ (π΅(reprβπ)π) β Fin)) |
15 | | sumss2 15669 |
. . . 4
β’
(((((π΄ β© π΅)(reprβπ)π) β (π΅(reprβπ)π) β§ βπ β ((π΄ β© π΅)(reprβπ)π)1 β β) β§ ((π΅(reprβπ)π) β (β€β₯β0)
β¨ (π΅(reprβπ)π) β Fin)) β Ξ£π β ((π΄ β© π΅)(reprβπ)π)1 = Ξ£π β (π΅(reprβπ)π)if(π β ((π΄ β© π΅)(reprβπ)π), 1, 0)) |
16 | 8, 13, 14, 15 | syl21anc 837 |
. . 3
β’ (π β Ξ£π β ((π΄ β© π΅)(reprβπ)π)1 = Ξ£π β (π΅(reprβπ)π)if(π β ((π΄ β© π΅)(reprβπ)π), 1, 0)) |
17 | 1, 2, 3 | reprinrn 33619 |
. . . . . . . 8
β’ (π β (π β ((π΅ β© π΄)(reprβπ)π) β (π β (π΅(reprβπ)π) β§ ran π β π΄))) |
18 | | incom 4201 |
. . . . . . . . . . . 12
β’ (π΅ β© π΄) = (π΄ β© π΅) |
19 | 18 | oveq1i 7416 |
. . . . . . . . . . 11
β’ ((π΅ β© π΄)(reprβπ)π) = ((π΄ β© π΅)(reprβπ)π) |
20 | 19 | eleq2i 2826 |
. . . . . . . . . 10
β’ (π β ((π΅ β© π΄)(reprβπ)π) β π β ((π΄ β© π΅)(reprβπ)π)) |
21 | 20 | bibi1i 339 |
. . . . . . . . 9
β’ ((π β ((π΅ β© π΄)(reprβπ)π) β (π β (π΅(reprβπ)π) β§ ran π β π΄)) β (π β ((π΄ β© π΅)(reprβπ)π) β (π β (π΅(reprβπ)π) β§ ran π β π΄))) |
22 | 21 | imbi2i 336 |
. . . . . . . 8
β’ ((π β (π β ((π΅ β© π΄)(reprβπ)π) β (π β (π΅(reprβπ)π) β§ ran π β π΄))) β (π β (π β ((π΄ β© π΅)(reprβπ)π) β (π β (π΅(reprβπ)π) β§ ran π β π΄)))) |
23 | 17, 22 | mpbi 229 |
. . . . . . 7
β’ (π β (π β ((π΄ β© π΅)(reprβπ)π) β (π β (π΅(reprβπ)π) β§ ran π β π΄))) |
24 | 23 | baibd 541 |
. . . . . 6
β’ ((π β§ π β (π΅(reprβπ)π)) β (π β ((π΄ β© π΅)(reprβπ)π) β ran π β π΄)) |
25 | 24 | ifbid 4551 |
. . . . 5
β’ ((π β§ π β (π΅(reprβπ)π)) β if(π β ((π΄ β© π΅)(reprβπ)π), 1, 0) = if(ran π β π΄, 1, 0)) |
26 | | nnex 12215 |
. . . . . . . . 9
β’ β
β V |
27 | 26 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
28 | 27 | ralrimivw 3151 |
. . . . . . 7
β’ (π β βπ β (π΅(reprβπ)π)β β V) |
29 | 28 | r19.21bi 3249 |
. . . . . 6
β’ ((π β§ π β (π΅(reprβπ)π)) β β β V) |
30 | | fzofi 13936 |
. . . . . . 7
β’
(0..^π) β
Fin |
31 | 30 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (π΅(reprβπ)π)) β (0..^π) β Fin) |
32 | | reprval.a |
. . . . . . 7
β’ (π β π΄ β β) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (π΅(reprβπ)π)) β π΄ β β) |
34 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π΅(reprβπ)π)) β π΅ β β) |
35 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π΅(reprβπ)π)) β π β β€) |
36 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π΅(reprβπ)π)) β π β
β0) |
37 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (π΅(reprβπ)π)) β π β (π΅(reprβπ)π)) |
38 | 34, 35, 36, 37 | reprf 33613 |
. . . . . . 7
β’ ((π β§ π β (π΅(reprβπ)π)) β π:(0..^π)βΆπ΅) |
39 | 38, 34 | fssd 6733 |
. . . . . 6
β’ ((π β§ π β (π΅(reprβπ)π)) β π:(0..^π)βΆβ) |
40 | 29, 31, 33, 39 | prodindf 33010 |
. . . . 5
β’ ((π β§ π β (π΅(reprβπ)π)) β βπ β (0..^π)(((πββ)βπ΄)β(πβπ)) = if(ran π β π΄, 1, 0)) |
41 | 25, 40 | eqtr4d 2776 |
. . . 4
β’ ((π β§ π β (π΅(reprβπ)π)) β if(π β ((π΄ β© π΅)(reprβπ)π), 1, 0) = βπ β (0..^π)(((πββ)βπ΄)β(πβπ))) |
42 | 41 | sumeq2dv 15646 |
. . 3
β’ (π β Ξ£π β (π΅(reprβπ)π)if(π β ((π΄ β© π΅)(reprβπ)π), 1, 0) = Ξ£π β (π΅(reprβπ)π)βπ β (0..^π)(((πββ)βπ΄)β(πβπ))) |
43 | 16, 42 | eqtrd 2773 |
. 2
β’ (π β Ξ£π β ((π΄ β© π΅)(reprβπ)π)1 = Ξ£π β (π΅(reprβπ)π)βπ β (0..^π)(((πββ)βπ΄)β(πβπ))) |
44 | | hashcl 14313 |
. . . . 5
β’ (((π΄ β© π΅)(reprβπ)π) β Fin β (β―β((π΄ β© π΅)(reprβπ)π)) β
β0) |
45 | 9, 44 | syl 17 |
. . . 4
β’ (π β (β―β((π΄ β© π΅)(reprβπ)π)) β
β0) |
46 | 45 | nn0cnd 12531 |
. . 3
β’ (π β (β―β((π΄ β© π΅)(reprβπ)π)) β β) |
47 | 46 | mulridd 11228 |
. 2
β’ (π β ((β―β((π΄ β© π΅)(reprβπ)π)) Β· 1) = (β―β((π΄ β© π΅)(reprβπ)π))) |
48 | 12, 43, 47 | 3eqtr3rd 2782 |
1
β’ (π β (β―β((π΄ β© π΅)(reprβπ)π)) = Ξ£π β (π΅(reprβπ)π)βπ β (0..^π)(((πββ)βπ΄)β(πβπ))) |