Step | Hyp | Ref
| Expression |
1 | | eulerpartlemgh.1 |
. 2
β’ π = βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) |
2 | | eulerpart.p |
. . . . . . . . . . 11
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
3 | | eulerpart.o |
. . . . . . . . . . 11
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
4 | | eulerpart.d |
. . . . . . . . . . 11
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
5 | | eulerpart.j |
. . . . . . . . . . 11
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
6 | | eulerpart.f |
. . . . . . . . . . 11
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
7 | | eulerpart.h |
. . . . . . . . . . 11
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
8 | | eulerpart.m |
. . . . . . . . . . 11
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
9 | | eulerpart.r |
. . . . . . . . . . 11
β’ π
= {π β£ (β‘π β β) β
Fin} |
10 | | eulerpart.t |
. . . . . . . . . . 11
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemt0 33009 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) |
12 | 11 | simp1bi 1146 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β π΄ β (β0
βm β)) |
13 | | elmapi 8794 |
. . . . . . . . 9
β’ (π΄ β (β0
βm β) β π΄:ββΆβ0) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β π΄:ββΆβ0) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π΄:ββΆβ0) |
16 | 15 | ffund 6677 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β Fun π΄) |
17 | | inss1 4193 |
. . . . . . . . 9
β’ ((β‘π΄ β β) β© π½) β (β‘π΄ β β) |
18 | | cnvimass 6038 |
. . . . . . . . . 10
β’ (β‘π΄ β β) β dom π΄ |
19 | 18, 14 | fssdm 6693 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β
β) |
20 | 17, 19 | sstrid 3960 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β ((β‘π΄ β β) β© π½) β β) |
21 | 20 | sselda 3949 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β β) |
22 | 14 | fdmd 6684 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β dom π΄ = β) |
23 | 22 | eleq2d 2824 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β (π‘ β dom π΄ β π‘ β β)) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β (π‘ β dom π΄ β π‘ β β)) |
25 | 21, 24 | mpbird 257 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β dom π΄) |
26 | | fvco 6944 |
. . . . . 6
β’ ((Fun
π΄ β§ π‘ β dom π΄) β ((bits β π΄)βπ‘) = (bitsβ(π΄βπ‘))) |
27 | 16, 25, 26 | syl2anc 585 |
. . . . 5
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β ((bits β π΄)βπ‘) = (bitsβ(π΄βπ‘))) |
28 | 27 | xpeq2d 5668 |
. . . 4
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β ({π‘} Γ ((bits β π΄)βπ‘)) = ({π‘} Γ (bitsβ(π΄βπ‘)))) |
29 | 28 | iuneq2dv 4983 |
. . 3
β’ (π΄ β (π β© π
) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ ((bits β π΄)βπ‘)) = βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))) |
30 | | eqid 2737 |
. . . 4
β’ βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ ((bits β π΄)βπ‘)) = βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ ((bits β π΄)βπ‘)) |
31 | 30 | marypha2lem2 9379 |
. . 3
β’ βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ ((bits β π΄)βπ‘)) = {β¨π‘, πβ© β£ (π‘ β ((β‘π΄ β β) β© π½) β§ π β ((bits β π΄)βπ‘))} |
32 | 29, 31 | eqtr3di 2792 |
. 2
β’ (π΄ β (π β© π
) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) = {β¨π‘, πβ© β£ (π‘ β ((β‘π΄ β β) β© π½) β§ π β ((bits β π΄)βπ‘))}) |
33 | 1, 32 | eqtrid 2789 |
1
β’ (π΄ β (π β© π
) β π = {β¨π‘, πβ© β£ (π‘ β ((β‘π΄ β β) β© π½) β§ π β ((bits β π΄)βπ‘))}) |