Step | Hyp | Ref
| Expression |
1 | | gsumzcl.f |
. . . . . . 7
β’ (π β πΉ:π΄βΆπ΅) |
2 | | gsumzcl.a |
. . . . . . 7
β’ (π β π΄ β π) |
3 | | gsumzcl.0 |
. . . . . . . . 9
β’ 0 =
(0gβπΊ) |
4 | 3 | fvexi 6861 |
. . . . . . . 8
β’ 0 β
V |
5 | 4 | a1i 11 |
. . . . . . 7
β’ (π β 0 β V) |
6 | | ssidd 3972 |
. . . . . . 7
β’ (π β (πΉ supp 0 ) β (πΉ supp 0 )) |
7 | 1, 2, 5, 6 | gsumcllem 19692 |
. . . . . 6
β’ ((π β§ (πΉ supp 0 ) = β
) β πΉ = (π β π΄ β¦ 0 )) |
8 | 7 | oveq2d 7378 |
. . . . 5
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
9 | | gsumzcl.g |
. . . . . . 7
β’ (π β πΊ β Mnd) |
10 | 3 | gsumz 18653 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
11 | 9, 2, 10 | syl2anc 585 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
12 | 11 | adantr 482 |
. . . . 5
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
(π β π΄ β¦ 0 )) = 0 ) |
13 | 8, 12 | eqtrd 2777 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
πΉ) = 0 ) |
14 | | gsumzcl.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
15 | 14, 3 | mndidcl 18578 |
. . . . . 6
β’ (πΊ β Mnd β 0 β π΅) |
16 | 9, 15 | syl 17 |
. . . . 5
β’ (π β 0 β π΅) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β 0 β π΅) |
18 | 13, 17 | eqeltrd 2838 |
. . 3
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
πΉ) β π΅) |
19 | 18 | ex 414 |
. 2
β’ (π β ((πΉ supp 0 ) = β
β (πΊ Ξ£g
πΉ) β π΅)) |
20 | | eqid 2737 |
. . . . . . 7
β’
(+gβπΊ) = (+gβπΊ) |
21 | | gsumzcl.z |
. . . . . . 7
β’ π = (CntzβπΊ) |
22 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΊ β Mnd) |
23 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π΄ β π) |
24 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΉ:π΄βΆπ΅) |
25 | | gsumzcl.c |
. . . . . . . 8
β’ (π β ran πΉ β (πβran πΉ)) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran πΉ β (πβran πΉ)) |
27 | | simprl 770 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(β―β(πΉ supp
0 ))
β β) |
28 | | f1of1 6788 |
. . . . . . . . 9
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 )) |
29 | 28 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 )) |
30 | | suppssdm 8113 |
. . . . . . . . . 10
β’ (πΉ supp 0 ) β dom πΉ |
31 | 30, 1 | fssdm 6693 |
. . . . . . . . 9
β’ (π β (πΉ supp 0 ) β π΄) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β π΄) |
33 | | f1ss 6749 |
. . . . . . . 8
β’ ((π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 ) β§ (πΉ supp 0 ) β π΄) β π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) |
34 | 29, 32, 33 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) |
35 | | ssid 3971 |
. . . . . . . 8
β’ (πΉ supp 0 ) β (πΉ supp 0 ) |
36 | | f1ofo 6796 |
. . . . . . . . . 10
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β π:(1...(β―β(πΉ supp 0 )))βontoβ(πΉ supp 0 )) |
37 | | forn 6764 |
. . . . . . . . . 10
β’ (π:(1...(β―β(πΉ supp 0 )))βontoβ(πΉ supp 0 ) β ran π = (πΉ supp 0 )) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β ran π = (πΉ supp 0 )) |
39 | 38 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran π = (πΉ supp 0 )) |
40 | 35, 39 | sseqtrrid 4002 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β ran π) |
41 | | eqid 2737 |
. . . . . . 7
β’ ((πΉ β π) supp 0 ) = ((πΉ β π) supp 0 ) |
42 | 14, 3, 20, 21, 22, 23, 24, 26, 27, 34, 40, 41 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
πΉ) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(πΉ supp 0 )))) |
43 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
44 | 27, 43 | eleqtrdi 2848 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(β―β(πΉ supp
0 ))
β (β€β₯β1)) |
45 | | f1f 6743 |
. . . . . . . . . 10
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄ β π:(1...(β―β(πΉ supp 0 )))βΆπ΄) |
46 | 34, 45 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))βΆπ΄) |
47 | | fco 6697 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π:(1...(β―β(πΉ supp 0 )))βΆπ΄) β (πΉ β π):(1...(β―β(πΉ supp 0 )))βΆπ΅) |
48 | 24, 46, 47 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ β π):(1...(β―β(πΉ supp 0 )))βΆπ΅) |
49 | 48 | ffvelcdmda 7040 |
. . . . . . 7
β’ (((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β§ π β
(1...(β―β(πΉ supp
0 ))))
β ((πΉ β π)βπ) β π΅) |
50 | 14, 20 | mndcl 18571 |
. . . . . . . . 9
β’ ((πΊ β Mnd β§ π β π΅ β§ π₯ β π΅) β (π(+gβπΊ)π₯) β π΅) |
51 | 50 | 3expb 1121 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ (π β π΅ β§ π₯ β π΅)) β (π(+gβπΊ)π₯) β π΅) |
52 | 22, 51 | sylan 581 |
. . . . . . 7
β’ (((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β§ (π β π΅ β§ π₯ β π΅)) β (π(+gβπΊ)π₯) β π΅) |
53 | 44, 49, 52 | seqcl 13935 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(seq1((+gβπΊ), (πΉ β π))β(β―β(πΉ supp 0 ))) β π΅) |
54 | 42, 53 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
πΉ) β π΅) |
55 | 54 | expr 458 |
. . . 4
β’ ((π β§ (β―β(πΉ supp 0 )) β β) β
(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (πΊ Ξ£g
πΉ) β π΅)) |
56 | 55 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―β(πΉ supp 0 )) β β) β
(βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (πΊ Ξ£g
πΉ) β π΅)) |
57 | 56 | expimpd 455 |
. 2
β’ (π β (((β―β(πΉ supp 0 )) β β β§
βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) β (πΊ Ξ£g
πΉ) β π΅)) |
58 | | gsumzcl2.w |
. . 3
β’ (π β (πΉ supp 0 ) β
Fin) |
59 | | fz1f1o 15602 |
. . 3
β’ ((πΉ supp 0 ) β Fin β
((πΉ supp 0 ) = β
β¨
((β―β(πΉ supp
0 ))
β β β§ βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )))) |
60 | 58, 59 | syl 17 |
. 2
β’ (π β ((πΉ supp 0 ) = β
β¨
((β―β(πΉ supp
0 ))
β β β§ βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )))) |
61 | 19, 57, 60 | mpjaod 859 |
1
β’ (π β (πΊ Ξ£g πΉ) β π΅) |