Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . . 5
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β π β π΅) |
2 | | gsumconst.b |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
3 | | eqid 2737 |
. . . . . 6
β’
(0gβπΊ) = (0gβπΊ) |
4 | | gsumconst.m |
. . . . . 6
β’ Β· =
(.gβπΊ) |
5 | 2, 3, 4 | mulg0 18886 |
. . . . 5
β’ (π β π΅ β (0 Β· π) = (0gβπΊ)) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (0 Β· π) = (0gβπΊ)) |
7 | | fveq2 6847 |
. . . . . . 7
β’ (π΄ = β
β
(β―βπ΄) =
(β―ββ
)) |
8 | 7 | adantl 483 |
. . . . . 6
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (β―βπ΄) =
(β―ββ
)) |
9 | | hash0 14274 |
. . . . . 6
β’
(β―ββ
) = 0 |
10 | 8, 9 | eqtrdi 2793 |
. . . . 5
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (β―βπ΄) = 0) |
11 | 10 | oveq1d 7377 |
. . . 4
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β ((β―βπ΄) Β· π) = (0 Β· π)) |
12 | | mpteq1 5203 |
. . . . . . . 8
β’ (π΄ = β
β (π β π΄ β¦ π) = (π β β
β¦ π)) |
13 | 12 | adantl 483 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (π β π΄ β¦ π) = (π β β
β¦ π)) |
14 | | mpt0 6648 |
. . . . . . 7
β’ (π β β
β¦ π) = β
|
15 | 13, 14 | eqtrdi 2793 |
. . . . . 6
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (π β π΄ β¦ π) = β
) |
16 | 15 | oveq2d 7378 |
. . . . 5
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (πΊ Ξ£g (π β π΄ β¦ π)) = (πΊ Ξ£g
β
)) |
17 | 3 | gsum0 18546 |
. . . . 5
β’ (πΊ Ξ£g
β
) = (0gβπΊ) |
18 | 16, 17 | eqtrdi 2793 |
. . . 4
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (πΊ Ξ£g (π β π΄ β¦ π)) = (0gβπΊ)) |
19 | 6, 11, 18 | 3eqtr4rd 2788 |
. . 3
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ π΄ = β
) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) |
20 | 19 | ex 414 |
. 2
β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (π΄ = β
β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π))) |
21 | | simprl 770 |
. . . . . . . 8
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
22 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
23 | 21, 22 | eleqtrdi 2848 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
24 | | simpr 486 |
. . . . . . . . 9
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β π₯ β (1...(β―βπ΄))) |
25 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π β π΅) |
26 | 25 | adantr 482 |
. . . . . . . . 9
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β π β π΅) |
27 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β
(1...(β―βπ΄))
β¦ π) = (π₯ β
(1...(β―βπ΄))
β¦ π) |
28 | 27 | fvmpt2 6964 |
. . . . . . . . 9
β’ ((π₯ β
(1...(β―βπ΄))
β§ π β π΅) β ((π₯ β (1...(β―βπ΄)) β¦ π)βπ₯) = π) |
29 | 24, 26, 28 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β ((π₯ β (1...(β―βπ΄)) β¦ π)βπ₯) = π) |
30 | | f1of 6789 |
. . . . . . . . . . . . 13
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
31 | 30 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
32 | 31 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (πβπ₯) β π΄) |
33 | 31 | feqmptd 6915 |
. . . . . . . . . . 11
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π = (π₯ β (1...(β―βπ΄)) β¦ (πβπ₯))) |
34 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π) = (π β π΄ β¦ π)) |
35 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π = (πβπ₯) β π = π) |
36 | 32, 33, 34, 35 | fmptco 7080 |
. . . . . . . . . 10
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π) β π) = (π₯ β (1...(β―βπ΄)) β¦ π)) |
37 | 36 | fveq1d 6849 |
. . . . . . . . 9
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (((π β π΄ β¦ π) β π)βπ₯) = ((π₯ β (1...(β―βπ΄)) β¦ π)βπ₯)) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π) β π)βπ₯) = ((π₯ β (1...(β―βπ΄)) β¦ π)βπ₯)) |
39 | | elfznn 13477 |
. . . . . . . . 9
β’ (π₯ β
(1...(β―βπ΄))
β π₯ β
β) |
40 | | fvconst2g 7156 |
. . . . . . . . 9
β’ ((π β π΅ β§ π₯ β β) β ((β Γ
{π})βπ₯) = π) |
41 | 25, 39, 40 | syl2an 597 |
. . . . . . . 8
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β ((β Γ {π})βπ₯) = π) |
42 | 29, 38, 41 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π) β π)βπ₯) = ((β Γ {π})βπ₯)) |
43 | 23, 42 | seqfveq 13939 |
. . . . . 6
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β
(seq1((+gβπΊ), ((π β π΄ β¦ π) β π))β(β―βπ΄)) = (seq1((+gβπΊ), (β Γ {π}))β(β―βπ΄))) |
44 | | eqid 2737 |
. . . . . . 7
β’
(+gβπΊ) = (+gβπΊ) |
45 | | eqid 2737 |
. . . . . . 7
β’
(CntzβπΊ) =
(CntzβπΊ) |
46 | | simpl1 1192 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β πΊ β Mnd) |
47 | | simpl2 1193 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π΄ β Fin) |
48 | 25 | adantr 482 |
. . . . . . . 8
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β π β π΅) |
49 | 48 | fmpttd 7068 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π):π΄βΆπ΅) |
50 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π(+gβπΊ)π) = (π(+gβπΊ)π)) |
51 | 2, 44, 45 | elcntzsn 19112 |
. . . . . . . . . . 11
β’ (π β π΅ β (π β ((CntzβπΊ)β{π}) β (π β π΅ β§ (π(+gβπΊ)π) = (π(+gβπΊ)π)))) |
52 | 25, 51 | syl 17 |
. . . . . . . . . 10
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β ((CntzβπΊ)β{π}) β (π β π΅ β§ (π(+gβπΊ)π) = (π(+gβπΊ)π)))) |
53 | 25, 50, 52 | mpbir2and 712 |
. . . . . . . . 9
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π β ((CntzβπΊ)β{π})) |
54 | 53 | snssd 4774 |
. . . . . . . 8
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β {π} β ((CntzβπΊ)β{π})) |
55 | | snidg 4625 |
. . . . . . . . . . . 12
β’ (π β π΅ β π β {π}) |
56 | 25, 55 | syl 17 |
. . . . . . . . . . 11
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π β {π}) |
57 | 56 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β π β {π}) |
58 | 57 | fmpttd 7068 |
. . . . . . . . 9
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π):π΄βΆ{π}) |
59 | 58 | frnd 6681 |
. . . . . . . 8
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ran (π β π΄ β¦ π) β {π}) |
60 | 45 | cntzidss 19125 |
. . . . . . . 8
β’ (({π} β ((CntzβπΊ)β{π}) β§ ran (π β π΄ β¦ π) β {π}) β ran (π β π΄ β¦ π) β ((CntzβπΊ)βran (π β π΄ β¦ π))) |
61 | 54, 59, 60 | syl2anc 585 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ran (π β π΄ β¦ π) β ((CntzβπΊ)βran (π β π΄ β¦ π))) |
62 | | f1of1 6788 |
. . . . . . . 8
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))β1-1βπ΄) |
63 | 62 | ad2antll 728 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1βπ΄) |
64 | | suppssdm 8113 |
. . . . . . . . 9
β’ ((π β π΄ β¦ π) supp (0gβπΊ)) β dom (π β π΄ β¦ π) |
65 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β π΄ β¦ π) = (π β π΄ β¦ π) |
66 | 65 | dmmptss 6198 |
. . . . . . . . . 10
β’ dom
(π β π΄ β¦ π) β π΄ |
67 | 66 | a1i 11 |
. . . . . . . . 9
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β dom (π β π΄ β¦ π) β π΄) |
68 | 64, 67 | sstrid 3960 |
. . . . . . . 8
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π) supp (0gβπΊ)) β π΄) |
69 | | f1ofo 6796 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βontoβπ΄) |
70 | | forn 6764 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΄))βontoβπ΄ β ran π = π΄) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β ran π = π΄) |
72 | 71 | ad2antll 728 |
. . . . . . . 8
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ran π = π΄) |
73 | 68, 72 | sseqtrrd 3990 |
. . . . . . 7
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π) supp (0gβπΊ)) β ran π) |
74 | | eqid 2737 |
. . . . . . 7
β’ (((π β π΄ β¦ π) β π) supp (0gβπΊ)) = (((π β π΄ β¦ π) β π) supp (0gβπΊ)) |
75 | 2, 3, 44, 45, 46, 47, 49, 61, 21, 63, 73, 74 | gsumval3 19691 |
. . . . . 6
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΊ Ξ£g (π β π΄ β¦ π)) = (seq1((+gβπΊ), ((π β π΄ β¦ π) β π))β(β―βπ΄))) |
76 | | eqid 2737 |
. . . . . . . 8
β’
seq1((+gβπΊ), (β Γ {π})) = seq1((+gβπΊ), (β Γ {π})) |
77 | 2, 44, 4, 76 | mulgnn 18887 |
. . . . . . 7
β’
(((β―βπ΄)
β β β§ π
β π΅) β
((β―βπ΄) Β· π) =
(seq1((+gβπΊ), (β Γ {π}))β(β―βπ΄))) |
78 | 21, 25, 77 | syl2anc 585 |
. . . . . 6
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((β―βπ΄) Β· π) = (seq1((+gβπΊ), (β Γ {π}))β(β―βπ΄))) |
79 | 43, 75, 78 | 3eqtr4d 2787 |
. . . . 5
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) |
80 | 79 | expr 458 |
. . . 4
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π))) |
81 | 80 | exlimdv 1937 |
. . 3
β’ (((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β§ (β―βπ΄) β β) β (βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π))) |
82 | 81 | expimpd 455 |
. 2
β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (((β―βπ΄) β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π))) |
83 | | fz1f1o 15602 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
84 | 83 | 3ad2ant2 1135 |
. 2
β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
85 | 20, 82, 84 | mpjaod 859 |
1
β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) |