Step | Hyp | Ref
| Expression |
1 | | gsumzcl.g |
. . . . . . 7
β’ (π β πΊ β Mnd) |
2 | | gsumzcl.a |
. . . . . . . 8
β’ (π β π΄ β π) |
3 | | inex1g 5281 |
. . . . . . . 8
β’ (π΄ β π β (π΄ β© π) β V) |
4 | 2, 3 | syl 17 |
. . . . . . 7
β’ (π β (π΄ β© π) β V) |
5 | | gsumzcl.0 |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
6 | 5 | gsumz 18653 |
. . . . . . 7
β’ ((πΊ β Mnd β§ (π΄ β© π) β V) β (πΊ Ξ£g (π β (π΄ β© π) β¦ 0 )) = 0 ) |
7 | 1, 4, 6 | syl2anc 585 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π β (π΄ β© π) β¦ 0 )) = 0 ) |
8 | 5 | gsumz 18653 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
9 | 1, 2, 8 | syl2anc 585 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
10 | 7, 9 | eqtr4d 2780 |
. . . . 5
β’ (π β (πΊ Ξ£g (π β (π΄ β© π) β¦ 0 )) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
(π β (π΄ β© π) β¦ 0 )) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
12 | | resres 5955 |
. . . . . . . 8
β’ ((πΉ βΎ π΄) βΎ π) = (πΉ βΎ (π΄ β© π)) |
13 | | gsumzcl.f |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆπ΅) |
14 | | ffn 6673 |
. . . . . . . . . 10
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
15 | | fnresdm 6625 |
. . . . . . . . . 10
β’ (πΉ Fn π΄ β (πΉ βΎ π΄) = πΉ) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . . 9
β’ (π β (πΉ βΎ π΄) = πΉ) |
17 | 16 | reseq1d 5941 |
. . . . . . . 8
β’ (π β ((πΉ βΎ π΄) βΎ π) = (πΉ βΎ π)) |
18 | 12, 17 | eqtr3id 2791 |
. . . . . . 7
β’ (π β (πΉ βΎ (π΄ β© π)) = (πΉ βΎ π)) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΉ βΎ (π΄ β© π)) = (πΉ βΎ π)) |
20 | 5 | fvexi 6861 |
. . . . . . . . . 10
β’ 0 β
V |
21 | 20 | a1i 11 |
. . . . . . . . 9
β’ (π β 0 β V) |
22 | | ssid 3971 |
. . . . . . . . . 10
β’ (πΉ supp 0 ) β (πΉ supp 0 ) |
23 | 22 | a1i 11 |
. . . . . . . . 9
β’ (π β (πΉ supp 0 ) β (πΉ supp 0 )) |
24 | 13, 2, 21, 23 | gsumcllem 19692 |
. . . . . . . 8
β’ ((π β§ (πΉ supp 0 ) = β
) β πΉ = (π β π΄ β¦ 0 )) |
25 | 24 | reseq1d 5941 |
. . . . . . 7
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΉ βΎ (π΄ β© π)) = ((π β π΄ β¦ 0 ) βΎ (π΄ β© π))) |
26 | | inss1 4193 |
. . . . . . . 8
β’ (π΄ β© π) β π΄ |
27 | | resmpt 5996 |
. . . . . . . 8
β’ ((π΄ β© π) β π΄ β ((π β π΄ β¦ 0 ) βΎ (π΄ β© π)) = (π β (π΄ β© π) β¦ 0 )) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
β’ ((π β π΄ β¦ 0 ) βΎ (π΄ β© π)) = (π β (π΄ β© π) β¦ 0 ) |
29 | 25, 28 | eqtrdi 2793 |
. . . . . 6
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΉ βΎ (π΄ β© π)) = (π β (π΄ β© π) β¦ 0 )) |
30 | 19, 29 | eqtr3d 2779 |
. . . . 5
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΉ βΎ π) = (π β (π΄ β© π) β¦ 0 )) |
31 | 30 | oveq2d 7378 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g (π β (π΄ β© π) β¦ 0 ))) |
32 | 24 | oveq2d 7378 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
33 | 11, 31, 32 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g πΉ)) |
34 | 33 | ex 414 |
. 2
β’ (π β ((πΉ supp 0 ) = β
β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g πΉ))) |
35 | | f1ofo 6796 |
. . . . . . . . . . . 12
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β π:(1...(β―β(πΉ supp 0 )))βontoβ(πΉ supp 0 )) |
36 | | forn 6764 |
. . . . . . . . . . . 12
β’ (π:(1...(β―β(πΉ supp 0 )))βontoβ(πΉ supp 0 ) β ran π = (πΉ supp 0 )) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β ran π = (πΉ supp 0 )) |
38 | 37 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran π = (πΉ supp 0 )) |
39 | | gsumzres.s |
. . . . . . . . . . 11
β’ (π β (πΉ supp 0 ) β π) |
40 | 39 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β π) |
41 | 38, 40 | eqsstrd 3987 |
. . . . . . . . 9
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran π β π) |
42 | | cores 6206 |
. . . . . . . . 9
β’ (ran
π β π β ((πΉ βΎ π) β π) = (πΉ β π)) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ((πΉ βΎ π) β π) = (πΉ β π)) |
44 | 43 | seqeq3d 13921 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
seq1((+gβπΊ), ((πΉ βΎ π) β π)) = seq1((+gβπΊ), (πΉ β π))) |
45 | 44 | fveq1d 6849 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(seq1((+gβπΊ), ((πΉ βΎ π) β π))β(β―β(πΉ supp 0 ))) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(πΉ supp 0 )))) |
46 | | gsumzcl.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
47 | | eqid 2737 |
. . . . . . 7
β’
(+gβπΊ) = (+gβπΊ) |
48 | | gsumzcl.z |
. . . . . . 7
β’ π = (CntzβπΊ) |
49 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΊ β Mnd) |
50 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (π΄ β© π) β V) |
51 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΉ:π΄βΆπ΅) |
52 | | fssres 6713 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ (π΄ β© π) β π΄) β (πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅) |
53 | 51, 26, 52 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅) |
54 | 18 | feq1d 6658 |
. . . . . . . . 9
β’ (π β ((πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅ β (πΉ βΎ π):(π΄ β© π)βΆπ΅)) |
55 | 54 | biimpa 478 |
. . . . . . . 8
β’ ((π β§ (πΉ βΎ (π΄ β© π)):(π΄ β© π)βΆπ΅) β (πΉ βΎ π):(π΄ β© π)βΆπ΅) |
56 | 53, 55 | syldan 592 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ βΎ π):(π΄ β© π)βΆπ΅) |
57 | | gsumzcl.c |
. . . . . . . . 9
β’ (π β ran πΉ β (πβran πΉ)) |
58 | | resss 5967 |
. . . . . . . . . 10
β’ (πΉ βΎ π) β πΉ |
59 | 58 | rnssi 5900 |
. . . . . . . . 9
β’ ran
(πΉ βΎ π) β ran πΉ |
60 | 48 | cntzidss 19125 |
. . . . . . . . 9
β’ ((ran
πΉ β (πβran πΉ) β§ ran (πΉ βΎ π) β ran πΉ) β ran (πΉ βΎ π) β (πβran (πΉ βΎ π))) |
61 | 57, 59, 60 | sylancl 587 |
. . . . . . . 8
β’ (π β ran (πΉ βΎ π) β (πβran (πΉ βΎ π))) |
62 | 61 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran (πΉ βΎ π) β (πβran (πΉ βΎ π))) |
63 | | simprl 770 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(β―β(πΉ supp
0 ))
β β) |
64 | | f1of1 6788 |
. . . . . . . . 9
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 )) |
65 | 64 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 )) |
66 | | suppssdm 8113 |
. . . . . . . . . . 11
β’ (πΉ supp 0 ) β dom πΉ |
67 | 66, 13 | fssdm 6693 |
. . . . . . . . . 10
β’ (π β (πΉ supp 0 ) β π΄) |
68 | 67, 39 | ssind 4197 |
. . . . . . . . 9
β’ (π β (πΉ supp 0 ) β (π΄ β© π)) |
69 | 68 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β (π΄ β© π)) |
70 | | f1ss 6749 |
. . . . . . . 8
β’ ((π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 ) β§ (πΉ supp 0 ) β (π΄ β© π)) β π:(1...(β―β(πΉ supp 0 )))β1-1β(π΄ β© π)) |
71 | 65, 69, 70 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1β(π΄ β© π)) |
72 | 13, 2 | fexd 7182 |
. . . . . . . . . . . 12
β’ (π β πΉ β V) |
73 | | ressuppss 8119 |
. . . . . . . . . . . 12
β’ ((πΉ β V β§ 0 β V)
β ((πΉ βΎ π) supp 0 ) β (πΉ supp 0 )) |
74 | 72, 20, 73 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β ((πΉ βΎ π) supp 0 ) β (πΉ supp 0 )) |
75 | | sseq2 3975 |
. . . . . . . . . . 11
β’ (ran
π = (πΉ supp 0 ) β (((πΉ βΎ π) supp 0 ) β ran π β ((πΉ βΎ π) supp 0 ) β (πΉ supp 0 ))) |
76 | 74, 75 | syl5ibr 246 |
. . . . . . . . . 10
β’ (ran
π = (πΉ supp 0 ) β (π β ((πΉ βΎ π) supp 0 ) β ran π)) |
77 | 35, 36, 76 | 3syl 18 |
. . . . . . . . 9
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (π β ((πΉ βΎ π) supp 0 ) β ran π)) |
78 | 77 | adantl 483 |
. . . . . . . 8
β’
(((β―β(πΉ
supp 0 ))
β β β§ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) β (π β ((πΉ βΎ π) supp 0 ) β ran π)) |
79 | 78 | impcom 409 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ((πΉ βΎ π) supp 0 ) β ran π) |
80 | | eqid 2737 |
. . . . . . 7
β’ (((πΉ βΎ π) β π) supp 0 ) = (((πΉ βΎ π) β π) supp 0 ) |
81 | 46, 5, 47, 48, 49, 50, 56, 62, 63, 71, 79, 80 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
(πΉ βΎ π)) =
(seq1((+gβπΊ), ((πΉ βΎ π) β π))β(β―β(πΉ supp 0 )))) |
82 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π΄ β π) |
83 | 57 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran πΉ β (πβran πΉ)) |
84 | 67 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β π΄) |
85 | | f1ss 6749 |
. . . . . . . 8
β’ ((π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 ) β§ (πΉ supp 0 ) β π΄) β π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) |
86 | 65, 84, 85 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) |
87 | 22, 38 | sseqtrrid 4002 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β ran π) |
88 | | eqid 2737 |
. . . . . . 7
β’ ((πΉ β π) supp 0 ) = ((πΉ β π) supp 0 ) |
89 | 46, 5, 47, 48, 49, 82, 51, 83, 63, 86, 87, 88 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
πΉ) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(πΉ supp 0 )))) |
90 | 45, 81, 89 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g πΉ)) |
91 | 90 | expr 458 |
. . . 4
β’ ((π β§ (β―β(πΉ supp 0 )) β β) β
(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g πΉ))) |
92 | 91 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―β(πΉ supp 0 )) β β) β
(βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g πΉ))) |
93 | 92 | expimpd 455 |
. 2
β’ (π β (((β―β(πΉ supp 0 )) β β β§
βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) β (πΊ Ξ£g
(πΉ βΎ π)) = (πΊ Ξ£g πΉ))) |
94 | | gsumzres.w |
. . 3
β’ (π β πΉ finSupp 0 ) |
95 | | fsuppimp 9318 |
. . . 4
β’ (πΉ finSupp 0 β (Fun πΉ β§ (πΉ supp 0 ) β
Fin)) |
96 | 95 | simprd 497 |
. . 3
β’ (πΉ finSupp 0 β (πΉ supp 0 ) β
Fin) |
97 | | fz1f1o 15602 |
. . 3
β’ ((πΉ supp 0 ) β Fin β
((πΉ supp 0 ) = β
β¨
((β―β(πΉ supp
0 ))
β β β§ βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )))) |
98 | 94, 96, 97 | 3syl 18 |
. 2
β’ (π β ((πΉ supp 0 ) = β
β¨
((β―β(πΉ supp
0 ))
β β β§ βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )))) |
99 | 34, 93, 98 | mpjaod 859 |
1
β’ (π β (πΊ Ξ£g (πΉ βΎ π)) = (πΊ Ξ£g πΉ)) |