Step | Hyp | Ref
| Expression |
1 | | prdsgsum.y |
. . . 4
β’ π = (πXs(π₯ β πΌ β¦ π
)) |
2 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
3 | | prdsgsum.s |
. . . 4
β’ (π β π β π) |
4 | | prdsgsum.i |
. . . 4
β’ (π β πΌ β π) |
5 | | prdsgsum.r |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β π
β CMnd) |
6 | 5 | fmpttd 7067 |
. . . . 5
β’ (π β (π₯ β πΌ β¦ π
):πΌβΆCMnd) |
7 | 6 | ffnd 6673 |
. . . 4
β’ (π β (π₯ β πΌ β¦ π
) Fn πΌ) |
8 | | prdsgsum.z |
. . . . 5
β’ 0 =
(0gβπ) |
9 | 1, 4, 3, 6 | prdscmnd 19647 |
. . . . 5
β’ (π β π β CMnd) |
10 | | prdsgsum.j |
. . . . 5
β’ (π β π½ β π) |
11 | | prdsgsum.f |
. . . . . . . . . 10
β’ ((π β§ (π₯ β πΌ β§ π¦ β π½)) β π β π΅) |
12 | 11 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΌ) β§ π¦ β π½) β π β π΅) |
13 | 12 | an32s 651 |
. . . . . . . 8
β’ (((π β§ π¦ β π½) β§ π₯ β πΌ) β π β π΅) |
14 | 13 | ralrimiva 3140 |
. . . . . . 7
β’ ((π β§ π¦ β π½) β βπ₯ β πΌ π β π΅) |
15 | 5 | ralrimiva 3140 |
. . . . . . . . 9
β’ (π β βπ₯ β πΌ π
β CMnd) |
16 | | prdsgsum.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ
) |
17 | 1, 2, 3, 4, 15, 16 | prdsbasmpt2 17372 |
. . . . . . . 8
β’ (π β ((π₯ β πΌ β¦ π) β (Baseβπ) β βπ₯ β πΌ π β π΅)) |
18 | 17 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π½) β ((π₯ β πΌ β¦ π) β (Baseβπ) β βπ₯ β πΌ π β π΅)) |
19 | 14, 18 | mpbird 257 |
. . . . . 6
β’ ((π β§ π¦ β π½) β (π₯ β πΌ β¦ π) β (Baseβπ)) |
20 | 19 | fmpttd 7067 |
. . . . 5
β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)):π½βΆ(Baseβπ)) |
21 | | prdsgsum.w |
. . . . 5
β’ (π β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) |
22 | 2, 8, 9, 10, 20, 21 | gsumcl 19700 |
. . . 4
β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) β (Baseβπ)) |
23 | 1, 2, 3, 4, 7, 22 | prdsbasfn 17361 |
. . 3
β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) Fn πΌ) |
24 | | nfcv 2904 |
. . . . 5
β’
β²π₯π |
25 | | nfcv 2904 |
. . . . 5
β’
β²π₯
Ξ£g |
26 | | nfcv 2904 |
. . . . . 6
β’
β²π₯π½ |
27 | | nfmpt1 5217 |
. . . . . 6
β’
β²π₯(π₯ β πΌ β¦ π) |
28 | 26, 27 | nfmpt 5216 |
. . . . 5
β’
β²π₯(π¦ β π½ β¦ (π₯ β πΌ β¦ π)) |
29 | 24, 25, 28 | nfov 7391 |
. . . 4
β’
β²π₯(π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) |
30 | 29 | dffn5f 6917 |
. . 3
β’ ((π Ξ£g
(π¦ β π½ β¦ (π₯ β πΌ β¦ π))) Fn πΌ β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ ((π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π)))βπ₯))) |
31 | 23, 30 | sylib 217 |
. 2
β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ ((π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π)))βπ₯))) |
32 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π₯ β πΌ) |
33 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β πΌ β¦ π) = (π₯ β πΌ β¦ π) |
34 | 33 | fvmpt2 6963 |
. . . . . . 7
β’ ((π₯ β πΌ β§ π β π΅) β ((π₯ β πΌ β¦ π)βπ₯) = π) |
35 | 32, 12, 34 | syl2an2r 684 |
. . . . . 6
β’ (((π β§ π₯ β πΌ) β§ π¦ β π½) β ((π₯ β πΌ β¦ π)βπ₯) = π) |
36 | 35 | mpteq2dva 5209 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (π¦ β π½ β¦ ((π₯ β πΌ β¦ π)βπ₯)) = (π¦ β π½ β¦ π)) |
37 | 36 | oveq2d 7377 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (π
Ξ£g (π¦ β π½ β¦ ((π₯ β πΌ β¦ π)βπ₯))) = (π
Ξ£g (π¦ β π½ β¦ π))) |
38 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β π β CMnd) |
39 | | cmnmnd 19587 |
. . . . . 6
β’ (π
β CMnd β π
β Mnd) |
40 | 5, 39 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β π
β Mnd) |
41 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β π½ β π) |
42 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β πΌ β π) |
43 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β π β π) |
44 | 40 | fmpttd 7067 |
. . . . . . . 8
β’ (π β (π₯ β πΌ β¦ π
):πΌβΆMnd) |
45 | 44 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β (π₯ β πΌ β¦ π
):πΌβΆMnd) |
46 | 1, 2, 42, 43, 45, 32 | prdspjmhm 18647 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (π β (Baseβπ) β¦ (πβπ₯)) β (π MndHom ((π₯ β πΌ β¦ π
)βπ₯))) |
47 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β πΌ β¦ π
) = (π₯ β πΌ β¦ π
) |
48 | 47 | fvmpt2 6963 |
. . . . . . . 8
β’ ((π₯ β πΌ β§ π
β CMnd) β ((π₯ β πΌ β¦ π
)βπ₯) = π
) |
49 | 32, 5, 48 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β πΌ) β ((π₯ β πΌ β¦ π
)βπ₯) = π
) |
50 | 49 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ π₯ β πΌ) β (π MndHom ((π₯ β πΌ β¦ π
)βπ₯)) = (π MndHom π
)) |
51 | 46, 50 | eleqtrd 2836 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (π β (Baseβπ) β¦ (πβπ₯)) β (π MndHom π
)) |
52 | 19 | adantlr 714 |
. . . . 5
β’ (((π β§ π₯ β πΌ) β§ π¦ β π½) β (π₯ β πΌ β¦ π) β (Baseβπ)) |
53 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β πΌ) β (π¦ β π½ β¦ (π₯ β πΌ β¦ π)) finSupp 0 ) |
54 | | fveq1 6845 |
. . . . 5
β’ (π = (π₯ β πΌ β¦ π) β (πβπ₯) = ((π₯ β πΌ β¦ π)βπ₯)) |
55 | | fveq1 6845 |
. . . . 5
β’ (π = (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) β (πβπ₯) = ((π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π)))βπ₯)) |
56 | 2, 8, 38, 40, 41, 51, 52, 53, 54, 55 | gsummhm2 19724 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (π
Ξ£g (π¦ β π½ β¦ ((π₯ β πΌ β¦ π)βπ₯))) = ((π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π)))βπ₯)) |
57 | 37, 56 | eqtr3d 2775 |
. . 3
β’ ((π β§ π₯ β πΌ) β (π
Ξ£g (π¦ β π½ β¦ π)) = ((π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π)))βπ₯)) |
58 | 57 | mpteq2dva 5209 |
. 2
β’ (π β (π₯ β πΌ β¦ (π
Ξ£g (π¦ β π½ β¦ π))) = (π₯ β πΌ β¦ ((π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π)))βπ₯))) |
59 | 31, 58 | eqtr4d 2776 |
1
β’ (π β (π Ξ£g (π¦ β π½ β¦ (π₯ β πΌ β¦ π))) = (π₯ β πΌ β¦ (π
Ξ£g (π¦ β π½ β¦ π)))) |