Step | Hyp | Ref
| Expression |
1 | | elinel2 4197 |
. . . . 5
β’ (π΄ β (π«
β0 β© Fin) β π΄ β Fin) |
2 | | 2nn0 12489 |
. . . . . . 7
β’ 2 β
β0 |
3 | 2 | a1i 11 |
. . . . . 6
β’ ((π΄ β (π«
β0 β© Fin) β§ π β π΄) β 2 β
β0) |
4 | | elfpw 9354 |
. . . . . . . 8
β’ (π΄ β (π«
β0 β© Fin) β (π΄ β β0 β§ π΄ β Fin)) |
5 | 4 | simplbi 499 |
. . . . . . 7
β’ (π΄ β (π«
β0 β© Fin) β π΄ β
β0) |
6 | 5 | sselda 3983 |
. . . . . 6
β’ ((π΄ β (π«
β0 β© Fin) β§ π β π΄) β π β β0) |
7 | 3, 6 | nn0expcld 14209 |
. . . . 5
β’ ((π΄ β (π«
β0 β© Fin) β§ π β π΄) β (2βπ) β
β0) |
8 | 1, 7 | fsumnn0cl 15682 |
. . . 4
β’ (π΄ β (π«
β0 β© Fin) β Ξ£π β π΄ (2βπ) β
β0) |
9 | | bitsinv1 16383 |
. . . 4
β’
(Ξ£π β
π΄ (2βπ) β β0
β Ξ£π β
(bitsβΞ£π β
π΄ (2βπ))(2βπ) = Ξ£π β π΄ (2βπ)) |
10 | 8, 9 | syl 17 |
. . 3
β’ (π΄ β (π«
β0 β© Fin) β Ξ£π β (bitsβΞ£π β π΄ (2βπ))(2βπ) = Ξ£π β π΄ (2βπ)) |
11 | | bitsss 16367 |
. . . . . 6
β’
(bitsβΞ£π
β π΄ (2βπ)) β
β0 |
12 | 11 | a1i 11 |
. . . . 5
β’ (π΄ β (π«
β0 β© Fin) β (bitsβΞ£π β π΄ (2βπ)) β
β0) |
13 | | bitsfi 16378 |
. . . . . 6
β’
(Ξ£π β
π΄ (2βπ) β β0
β (bitsβΞ£π
β π΄ (2βπ)) β Fin) |
14 | 8, 13 | syl 17 |
. . . . 5
β’ (π΄ β (π«
β0 β© Fin) β (bitsβΞ£π β π΄ (2βπ)) β Fin) |
15 | | elfpw 9354 |
. . . . 5
β’
((bitsβΞ£π β π΄ (2βπ)) β (π« β0
β© Fin) β ((bitsβΞ£π β π΄ (2βπ)) β β0 β§
(bitsβΞ£π β
π΄ (2βπ)) β Fin)) |
16 | 12, 14, 15 | sylanbrc 584 |
. . . 4
β’ (π΄ β (π«
β0 β© Fin) β (bitsβΞ£π β π΄ (2βπ)) β (π« β0
β© Fin)) |
17 | | oveq2 7417 |
. . . . . . 7
β’ (π = π β (2βπ) = (2βπ)) |
18 | 17 | cbvsumv 15642 |
. . . . . 6
β’
Ξ£π β
π (2βπ) = Ξ£π β π (2βπ) |
19 | | sumeq1 15635 |
. . . . . 6
β’ (π = (bitsβΞ£π β π΄ (2βπ)) β Ξ£π β π (2βπ) = Ξ£π β (bitsβΞ£π β π΄ (2βπ))(2βπ)) |
20 | 18, 19 | eqtrid 2785 |
. . . . 5
β’ (π = (bitsβΞ£π β π΄ (2βπ)) β Ξ£π β π (2βπ) = Ξ£π β (bitsβΞ£π β π΄ (2βπ))(2βπ)) |
21 | | eqid 2733 |
. . . . 5
β’ (π β (π«
β0 β© Fin) β¦ Ξ£π β π (2βπ)) = (π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ)) |
22 | | sumex 15634 |
. . . . 5
β’
Ξ£π β
(bitsβΞ£π β
π΄ (2βπ))(2βπ) β V |
23 | 20, 21, 22 | fvmpt 6999 |
. . . 4
β’
((bitsβΞ£π β π΄ (2βπ)) β (π« β0
β© Fin) β ((π
β (π« β0 β© Fin) β¦ Ξ£π β π (2βπ))β(bitsβΞ£π β π΄ (2βπ))) = Ξ£π β (bitsβΞ£π β π΄ (2βπ))(2βπ)) |
24 | 16, 23 | syl 17 |
. . 3
β’ (π΄ β (π«
β0 β© Fin) β ((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))β(bitsβΞ£π β π΄ (2βπ))) = Ξ£π β (bitsβΞ£π β π΄ (2βπ))(2βπ)) |
25 | | sumeq1 15635 |
. . . 4
β’ (π = π΄ β Ξ£π β π (2βπ) = Ξ£π β π΄ (2βπ)) |
26 | | sumex 15634 |
. . . 4
β’
Ξ£π β
π΄ (2βπ) β V |
27 | 25, 21, 26 | fvmpt 6999 |
. . 3
β’ (π΄ β (π«
β0 β© Fin) β ((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))βπ΄) = Ξ£π β π΄ (2βπ)) |
28 | 10, 24, 27 | 3eqtr4d 2783 |
. 2
β’ (π΄ β (π«
β0 β© Fin) β ((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))β(bitsβΞ£π β π΄ (2βπ))) = ((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))βπ΄)) |
29 | 21 | ackbijnn 15774 |
. . . 4
β’ (π β (π«
β0 β© Fin) β¦ Ξ£π β π (2βπ)):(π« β0 β©
Fin)β1-1-ontoββ0 |
30 | | f1of1 6833 |
. . . 4
β’ ((π β (π«
β0 β© Fin) β¦ Ξ£π β π (2βπ)):(π« β0 β©
Fin)β1-1-ontoββ0 β (π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ)):(π«
β0 β© Fin)β1-1ββ0) |
31 | 29, 30 | mp1i 13 |
. . 3
β’ (π΄ β (π«
β0 β© Fin) β (π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ)):(π«
β0 β© Fin)β1-1ββ0) |
32 | | id 22 |
. . 3
β’ (π΄ β (π«
β0 β© Fin) β π΄ β (π« β0 β©
Fin)) |
33 | | f1fveq 7261 |
. . 3
β’ (((π β (π«
β0 β© Fin) β¦ Ξ£π β π (2βπ)):(π« β0 β©
Fin)β1-1ββ0
β§ ((bitsβΞ£π
β π΄ (2βπ)) β (π«
β0 β© Fin) β§ π΄ β (π« β0 β©
Fin))) β (((π β
(π« β0 β© Fin) β¦ Ξ£π β π (2βπ))β(bitsβΞ£π β π΄ (2βπ))) = ((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))βπ΄) β (bitsβΞ£π β π΄ (2βπ)) = π΄)) |
34 | 31, 16, 32, 33 | syl12anc 836 |
. 2
β’ (π΄ β (π«
β0 β© Fin) β (((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))β(bitsβΞ£π β π΄ (2βπ))) = ((π β (π« β0 β©
Fin) β¦ Ξ£π
β π (2βπ))βπ΄) β (bitsβΞ£π β π΄ (2βπ)) = π΄)) |
35 | 28, 34 | mpbid 231 |
1
β’ (π΄ β (π«
β0 β© Fin) β (bitsβΞ£π β π΄ (2βπ)) = π΄) |