Step | Hyp | Ref
| Expression |
1 | | gsumzunsnd.b |
. . 3
β’ π΅ = (BaseβπΊ) |
2 | | eqid 2733 |
. . 3
β’
(0gβπΊ) = (0gβπΊ) |
3 | | gsumzunsnd.p |
. . 3
β’ + =
(+gβπΊ) |
4 | | gsumzunsnd.z |
. . 3
β’ π = (CntzβπΊ) |
5 | | gsumzunsnd.g |
. . 3
β’ (π β πΊ β Mnd) |
6 | | gsumzunsnd.a |
. . . 4
β’ (π β π΄ β Fin) |
7 | | snfi 8994 |
. . . 4
β’ {π} β Fin |
8 | | unfi 9122 |
. . . 4
β’ ((π΄ β Fin β§ {π} β Fin) β (π΄ βͺ {π}) β Fin) |
9 | 6, 7, 8 | sylancl 587 |
. . 3
β’ (π β (π΄ βͺ {π}) β Fin) |
10 | | elun 4112 |
. . . . 5
β’ (π β (π΄ βͺ {π}) β (π β π΄ β¨ π β {π})) |
11 | | gsumzunsnd.x |
. . . . . 6
β’ ((π β§ π β π΄) β π β π΅) |
12 | | elsni 4607 |
. . . . . . . 8
β’ (π β {π} β π = π) |
13 | | gsumzunsnd.s |
. . . . . . . 8
β’ ((π β§ π = π) β π = π) |
14 | 12, 13 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β {π}) β π = π) |
15 | | gsumzunsnd.y |
. . . . . . . 8
β’ (π β π β π΅) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β {π}) β π β π΅) |
17 | 14, 16 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π β {π}) β π β π΅) |
18 | 11, 17 | jaodan 957 |
. . . . 5
β’ ((π β§ (π β π΄ β¨ π β {π})) β π β π΅) |
19 | 10, 18 | sylan2b 595 |
. . . 4
β’ ((π β§ π β (π΄ βͺ {π})) β π β π΅) |
20 | | gsumzunsnd.f |
. . . 4
β’ πΉ = (π β (π΄ βͺ {π}) β¦ π) |
21 | 19, 20 | fmptd 7066 |
. . 3
β’ (π β πΉ:(π΄ βͺ {π})βΆπ΅) |
22 | | gsumzunsnd.c |
. . 3
β’ (π β ran πΉ β (πβran πΉ)) |
23 | 11 | expcom 415 |
. . . . . . 7
β’ (π β π΄ β (π β π β π΅)) |
24 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π = π) β π β π΅) |
25 | 13, 24 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π = π) β π β π΅) |
26 | 25 | expcom 415 |
. . . . . . . 8
β’ (π = π β (π β π β π΅)) |
27 | 12, 26 | syl 17 |
. . . . . . 7
β’ (π β {π} β (π β π β π΅)) |
28 | 23, 27 | jaoi 856 |
. . . . . 6
β’ ((π β π΄ β¨ π β {π}) β (π β π β π΅)) |
29 | 10, 28 | sylbi 216 |
. . . . 5
β’ (π β (π΄ βͺ {π}) β (π β π β π΅)) |
30 | 29 | impcom 409 |
. . . 4
β’ ((π β§ π β (π΄ βͺ {π})) β π β π΅) |
31 | | fvexd 6861 |
. . . 4
β’ (π β (0gβπΊ) β V) |
32 | 20, 9, 30, 31 | fsuppmptdm 9324 |
. . 3
β’ (π β πΉ finSupp (0gβπΊ)) |
33 | | gsumzunsnd.d |
. . . 4
β’ (π β Β¬ π β π΄) |
34 | | disjsn 4676 |
. . . 4
β’ ((π΄ β© {π}) = β
β Β¬ π β π΄) |
35 | 33, 34 | sylibr 233 |
. . 3
β’ (π β (π΄ β© {π}) = β
) |
36 | | eqidd 2734 |
. . 3
β’ (π β (π΄ βͺ {π}) = (π΄ βͺ {π})) |
37 | 1, 2, 3, 4, 5, 9, 21, 22, 32, 35, 36 | gsumzsplit 19712 |
. 2
β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (πΉ βΎ π΄)) + (πΊ Ξ£g (πΉ βΎ {π})))) |
38 | 20 | reseq1i 5937 |
. . . . 5
β’ (πΉ βΎ π΄) = ((π β (π΄ βͺ {π}) β¦ π) βΎ π΄) |
39 | | ssun1 4136 |
. . . . . 6
β’ π΄ β (π΄ βͺ {π}) |
40 | | resmpt 5995 |
. . . . . 6
β’ (π΄ β (π΄ βͺ {π}) β ((π β (π΄ βͺ {π}) β¦ π) βΎ π΄) = (π β π΄ β¦ π)) |
41 | 39, 40 | mp1i 13 |
. . . . 5
β’ (π β ((π β (π΄ βͺ {π}) β¦ π) βΎ π΄) = (π β π΄ β¦ π)) |
42 | 38, 41 | eqtrid 2785 |
. . . 4
β’ (π β (πΉ βΎ π΄) = (π β π΄ β¦ π)) |
43 | 42 | oveq2d 7377 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ π΄)) = (πΊ Ξ£g (π β π΄ β¦ π))) |
44 | 20 | reseq1i 5937 |
. . . . 5
β’ (πΉ βΎ {π}) = ((π β (π΄ βͺ {π}) β¦ π) βΎ {π}) |
45 | | ssun2 4137 |
. . . . . 6
β’ {π} β (π΄ βͺ {π}) |
46 | | resmpt 5995 |
. . . . . 6
β’ ({π} β (π΄ βͺ {π}) β ((π β (π΄ βͺ {π}) β¦ π) βΎ {π}) = (π β {π} β¦ π)) |
47 | 45, 46 | mp1i 13 |
. . . . 5
β’ (π β ((π β (π΄ βͺ {π}) β¦ π) βΎ {π}) = (π β {π} β¦ π)) |
48 | 44, 47 | eqtrid 2785 |
. . . 4
β’ (π β (πΉ βΎ {π}) = (π β {π} β¦ π)) |
49 | 48 | oveq2d 7377 |
. . 3
β’ (π β (πΊ Ξ£g (πΉ βΎ {π})) = (πΊ Ξ£g (π β {π} β¦ π))) |
50 | 43, 49 | oveq12d 7379 |
. 2
β’ (π β ((πΊ Ξ£g (πΉ βΎ π΄)) + (πΊ Ξ£g (πΉ βΎ {π}))) = ((πΊ Ξ£g (π β π΄ β¦ π)) + (πΊ Ξ£g (π β {π} β¦ π)))) |
51 | | gsumzunsnd.m |
. . . 4
β’ (π β π β π) |
52 | 1, 5, 51, 15, 13 | gsumsnd 19737 |
. . 3
β’ (π β (πΊ Ξ£g (π β {π} β¦ π)) = π) |
53 | 52 | oveq2d 7377 |
. 2
β’ (π β ((πΊ Ξ£g (π β π΄ β¦ π)) + (πΊ Ξ£g (π β {π} β¦ π))) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) |
54 | 37, 50, 53 | 3eqtrd 2777 |
1
β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (π β π΄ β¦ π)) + π)) |