Step | Hyp | Ref
| Expression |
1 | | cnfldbas 21244 |
. . . 4
β’ β =
(Baseββfld) |
2 | | cnfld0 21281 |
. . . 4
β’ 0 =
(0gββfld) |
3 | | cnring 21279 |
. . . . 5
β’
βfld β Ring |
4 | | ringcmn 20181 |
. . . . 5
β’
(βfld β Ring β βfld β
CMnd) |
5 | 3, 4 | mp1i 13 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β βfld β
CMnd) |
6 | | simp3 1135 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β πΌ β π) |
7 | | simp1 1133 |
. . . . 5
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β πΉ:πΌβΆβ) |
8 | | ax-resscn 11169 |
. . . . 5
β’ β
β β |
9 | | fss 6728 |
. . . . 5
β’ ((πΉ:πΌβΆβ β§ β β
β) β πΉ:πΌβΆβ) |
10 | 7, 8, 9 | sylancl 585 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β πΉ:πΌβΆβ) |
11 | | ssidd 4000 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (πΉ supp 0) β (πΉ supp 0)) |
12 | | simp2 1134 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β πΉ finSupp 0) |
13 | 1, 2, 5, 6, 10, 11, 12 | gsumres 19833 |
. . 3
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld
Ξ£g (πΉ βΎ (πΉ supp 0))) = (βfld
Ξ£g πΉ)) |
14 | | cnfldadd 21246 |
. . . 4
β’ + =
(+gββfld) |
15 | | df-refld 21498 |
. . . 4
β’
βfld = (βfld βΎs
β) |
16 | 8 | a1i 11 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β β β
β) |
17 | | 0red 11221 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β 0 β β) |
18 | | simpr 484 |
. . . . . 6
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β β) β π₯ β β) |
19 | 18 | addlidd 11419 |
. . . . 5
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β β) β (0 + π₯) = π₯) |
20 | 18 | addridd 11418 |
. . . . 5
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β β) β (π₯ + 0) = π₯) |
21 | 19, 20 | jca 511 |
. . . 4
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β β) β ((0 + π₯) = π₯ β§ (π₯ + 0) = π₯)) |
22 | 1, 14, 15, 5, 6, 16, 7, 17, 21 | gsumress 18615 |
. . 3
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld
Ξ£g πΉ) = (βfld
Ξ£g πΉ)) |
23 | 13, 22 | eqtr2d 2767 |
. 2
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld
Ξ£g πΉ) = (βfld
Ξ£g (πΉ βΎ (πΉ supp 0)))) |
24 | | suppssdm 8162 |
. . . . 5
β’ (πΉ supp 0) β dom πΉ |
25 | 24, 7 | fssdm 6731 |
. . . 4
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (πΉ supp 0) β πΌ) |
26 | 7, 25 | feqresmpt 6955 |
. . 3
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (πΉ βΎ (πΉ supp 0)) = (π₯ β (πΉ supp 0) β¦ (πΉβπ₯))) |
27 | 26 | oveq2d 7421 |
. 2
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld
Ξ£g (πΉ βΎ (πΉ supp 0))) = (βfld
Ξ£g (π₯ β (πΉ supp 0) β¦ (πΉβπ₯)))) |
28 | 12 | fsuppimpd 9371 |
. . 3
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (πΉ supp 0) β Fin) |
29 | | simpl1 1188 |
. . . . 5
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β (πΉ supp 0)) β πΉ:πΌβΆβ) |
30 | 25 | sselda 3977 |
. . . . 5
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β (πΉ supp 0)) β π₯ β πΌ) |
31 | 29, 30 | ffvelcdmd 7081 |
. . . 4
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β (πΉ supp 0)) β (πΉβπ₯) β β) |
32 | 8, 31 | sselid 3975 |
. . 3
β’ (((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β§ π₯ β (πΉ supp 0)) β (πΉβπ₯) β β) |
33 | 28, 32 | gsumfsum 21328 |
. 2
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld
Ξ£g (π₯ β (πΉ supp 0) β¦ (πΉβπ₯))) = Ξ£π₯ β (πΉ supp 0)(πΉβπ₯)) |
34 | 23, 27, 33 | 3eqtrd 2770 |
1
β’ ((πΉ:πΌβΆβ β§ πΉ finSupp 0 β§ πΌ β π) β (βfld
Ξ£g πΉ) = Ξ£π₯ β (πΉ supp 0)(πΉβπ₯)) |