Step | Hyp | Ref
| Expression |
1 | | gsumzcl.g |
. . . . . . 7
β’ (π β πΊ β Mnd) |
2 | | gsumzcl.a |
. . . . . . 7
β’ (π β π΄ β π) |
3 | | gsumzcl.0 |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
4 | 3 | gsumz 18653 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 585 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
6 | | gsumzf1o.h |
. . . . . . . . 9
β’ (π β π»:πΆβ1-1-ontoβπ΄) |
7 | | f1of1 6788 |
. . . . . . . . 9
β’ (π»:πΆβ1-1-ontoβπ΄ β π»:πΆβ1-1βπ΄) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (π β π»:πΆβ1-1βπ΄) |
9 | | f1dmex 7894 |
. . . . . . . 8
β’ ((π»:πΆβ1-1βπ΄ β§ π΄ β π) β πΆ β V) |
10 | 8, 2, 9 | syl2anc 585 |
. . . . . . 7
β’ (π β πΆ β V) |
11 | 3 | gsumz 18653 |
. . . . . . 7
β’ ((πΊ β Mnd β§ πΆ β V) β (πΊ Ξ£g
(π₯ β πΆ β¦ 0 )) = 0 ) |
12 | 1, 10, 11 | syl2anc 585 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π₯ β πΆ β¦ 0 )) = 0 ) |
13 | 5, 12 | eqtr4d 2780 |
. . . . 5
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = (πΊ Ξ£g (π₯ β πΆ β¦ 0 ))) |
14 | 13 | adantr 482 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
(π β π΄ β¦ 0 )) = (πΊ Ξ£g (π₯ β πΆ β¦ 0 ))) |
15 | | gsumzcl.f |
. . . . . 6
β’ (π β πΉ:π΄βΆπ΅) |
16 | 3 | fvexi 6861 |
. . . . . . 7
β’ 0 β
V |
17 | 16 | a1i 11 |
. . . . . 6
β’ (π β 0 β V) |
18 | | ssidd 3972 |
. . . . . 6
β’ (π β (πΉ supp 0 ) β (πΉ supp 0 )) |
19 | 15, 2, 17, 18 | gsumcllem 19692 |
. . . . 5
β’ ((π β§ (πΉ supp 0 ) = β
) β πΉ = (π β π΄ β¦ 0 )) |
20 | 19 | oveq2d 7378 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
21 | | f1of 6789 |
. . . . . . . . 9
β’ (π»:πΆβ1-1-ontoβπ΄ β π»:πΆβΆπ΄) |
22 | 6, 21 | syl 17 |
. . . . . . . 8
β’ (π β π»:πΆβΆπ΄) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉ supp 0 ) = β
) β π»:πΆβΆπ΄) |
24 | 23 | ffvelcdmda 7040 |
. . . . . 6
β’ (((π β§ (πΉ supp 0 ) = β
) β§ π₯ β πΆ) β (π»βπ₯) β π΄) |
25 | 23 | feqmptd 6915 |
. . . . . 6
β’ ((π β§ (πΉ supp 0 ) = β
) β π» = (π₯ β πΆ β¦ (π»βπ₯))) |
26 | | eqidd 2738 |
. . . . . 6
β’ (π = (π»βπ₯) β 0 = 0 ) |
27 | 24, 25, 19, 26 | fmptco 7080 |
. . . . 5
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΉ β π») = (π₯ β πΆ β¦ 0 )) |
28 | 27 | oveq2d 7378 |
. . . 4
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
(πΉ β π»)) = (πΊ Ξ£g (π₯ β πΆ β¦ 0 ))) |
29 | 14, 20, 28 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (πΉ supp 0 ) = β
) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (πΉ β π»))) |
30 | 29 | ex 414 |
. 2
β’ (π β ((πΉ supp 0 ) = β
β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (πΉ β π»)))) |
31 | 6 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π»:πΆβ1-1-ontoβπ΄) |
32 | | f1ococnv2 6816 |
. . . . . . . . . . . . . 14
β’ (π»:πΆβ1-1-ontoβπ΄ β (π» β β‘π») = ( I βΎ π΄)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (π» β β‘π») = ( I βΎ π΄)) |
34 | 33 | coeq1d 5822 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ((π» β β‘π») β π) = (( I βΎ π΄) β π)) |
35 | | f1of1 6788 |
. . . . . . . . . . . . . . 15
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 )) |
36 | 35 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 )) |
37 | | suppssdm 8113 |
. . . . . . . . . . . . . . . 16
β’ (πΉ supp 0 ) β dom πΉ |
38 | 37, 15 | fssdm 6693 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ supp 0 ) β π΄) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β π΄) |
40 | | f1ss 6749 |
. . . . . . . . . . . . . 14
β’ ((π:(1...(β―β(πΉ supp 0 )))β1-1β(πΉ supp 0 ) β§ (πΉ supp 0 ) β π΄) β π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) |
41 | 36, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) |
42 | | f1f 6743 |
. . . . . . . . . . . . 13
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄ β π:(1...(β―β(πΉ supp 0 )))βΆπ΄) |
43 | | fcoi2 6722 |
. . . . . . . . . . . . 13
β’ (π:(1...(β―β(πΉ supp 0 )))βΆπ΄ β (( I βΎ π΄) β π) = π) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (( I βΎ
π΄) β π) = π) |
45 | 34, 44 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ((π» β β‘π») β π) = π) |
46 | | coass 6222 |
. . . . . . . . . . 11
β’ ((π» β β‘π») β π) = (π» β (β‘π» β π)) |
47 | 45, 46 | eqtr3di 2792 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π = (π» β (β‘π» β π))) |
48 | 47 | coeq2d 5823 |
. . . . . . . . 9
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ β π) = (πΉ β (π» β (β‘π» β π)))) |
49 | | coass 6222 |
. . . . . . . . 9
β’ ((πΉ β π») β (β‘π» β π)) = (πΉ β (π» β (β‘π» β π))) |
50 | 48, 49 | eqtr4di 2795 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ β π) = ((πΉ β π») β (β‘π» β π))) |
51 | 50 | seqeq3d 13921 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
seq1((+gβπΊ), (πΉ β π)) = seq1((+gβπΊ), ((πΉ β π») β (β‘π» β π)))) |
52 | 51 | fveq1d 6849 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(seq1((+gβπΊ), (πΉ β π))β(β―β(πΉ supp 0 ))) =
(seq1((+gβπΊ), ((πΉ β π») β (β‘π» β π)))β(β―β(πΉ supp 0 )))) |
53 | | gsumzcl.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
54 | | eqid 2737 |
. . . . . . 7
β’
(+gβπΊ) = (+gβπΊ) |
55 | | gsumzcl.z |
. . . . . . 7
β’ π = (CntzβπΊ) |
56 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΊ β Mnd) |
57 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β π΄ β π) |
58 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΉ:π΄βΆπ΅) |
59 | | gsumzcl.c |
. . . . . . . 8
β’ (π β ran πΉ β (πβran πΉ)) |
60 | 59 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran πΉ β (πβran πΉ)) |
61 | | simprl 770 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β
(β―β(πΉ supp
0 ))
β β) |
62 | | ssid 3971 |
. . . . . . . 8
β’ (πΉ supp 0 ) β (πΉ supp 0 ) |
63 | | f1ofo 6796 |
. . . . . . . . . 10
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β π:(1...(β―β(πΉ supp 0 )))βontoβ(πΉ supp 0 )) |
64 | | forn 6764 |
. . . . . . . . . 10
β’ (π:(1...(β―β(πΉ supp 0 )))βontoβ(πΉ supp 0 ) β ran π = (πΉ supp 0 )) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
β’ (π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β ran π = (πΉ supp 0 )) |
66 | 65 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran π = (πΉ supp 0 )) |
67 | 62, 66 | sseqtrrid 4002 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β ran π) |
68 | | eqid 2737 |
. . . . . . 7
β’ ((πΉ β π) supp 0 ) = ((πΉ β π) supp 0 ) |
69 | 53, 3, 54, 55, 56, 57, 58, 60, 61, 41, 67, 68 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
πΉ) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(πΉ supp 0 )))) |
70 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β πΆ β V) |
71 | | fco 6697 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π»:πΆβΆπ΄) β (πΉ β π»):πΆβΆπ΅) |
72 | 15, 22, 71 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΉ β π»):πΆβΆπ΅) |
73 | 72 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ β π»):πΆβΆπ΅) |
74 | | rncoss 5932 |
. . . . . . . . 9
β’ ran
(πΉ β π») β ran πΉ |
75 | 55 | cntzidss 19125 |
. . . . . . . . 9
β’ ((ran
πΉ β (πβran πΉ) β§ ran (πΉ β π») β ran πΉ) β ran (πΉ β π») β (πβran (πΉ β π»))) |
76 | 59, 74, 75 | sylancl 587 |
. . . . . . . 8
β’ (π β ran (πΉ β π») β (πβran (πΉ β π»))) |
77 | 76 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ran (πΉ β π») β (πβran (πΉ β π»))) |
78 | | f1ocnv 6801 |
. . . . . . . . . 10
β’ (π»:πΆβ1-1-ontoβπ΄ β β‘π»:π΄β1-1-ontoβπΆ) |
79 | | f1of1 6788 |
. . . . . . . . . 10
β’ (β‘π»:π΄β1-1-ontoβπΆ β β‘π»:π΄β1-1βπΆ) |
80 | 6, 78, 79 | 3syl 18 |
. . . . . . . . 9
β’ (π β β‘π»:π΄β1-1βπΆ) |
81 | 80 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β β‘π»:π΄β1-1βπΆ) |
82 | | f1co 6755 |
. . . . . . . 8
β’ ((β‘π»:π΄β1-1βπΆ β§ π:(1...(β―β(πΉ supp 0 )))β1-1βπ΄) β (β‘π» β π):(1...(β―β(πΉ supp 0 )))β1-1βπΆ) |
83 | 81, 41, 82 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (β‘π» β π):(1...(β―β(πΉ supp 0 )))β1-1βπΆ) |
84 | | ssidd 3972 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΉ supp 0 ) β (πΉ supp 0 )) |
85 | 15, 2 | fexd 7182 |
. . . . . . . . . . . . . 14
β’ (π β πΉ β V) |
86 | | suppimacnv 8110 |
. . . . . . . . . . . . . 14
β’ ((πΉ β V β§ 0 β V)
β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
87 | 85, 16, 86 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
88 | 87 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (π β (β‘πΉ β (V β { 0 })) = (πΉ supp 0 )) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (β‘πΉ β (V β { 0 })) = (πΉ supp 0 )) |
90 | 84, 89, 66 | 3sstr4d 3996 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (β‘πΉ β (V β { 0 })) β ran π) |
91 | | imass2 6059 |
. . . . . . . . . 10
β’ ((β‘πΉ β (V β { 0 })) β ran π β (β‘π» β (β‘πΉ β (V β { 0 }))) β (β‘π» β ran π)) |
92 | 90, 91 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (β‘π» β (β‘πΉ β (V β { 0 }))) β (β‘π» β ran π)) |
93 | | cnvco 5846 |
. . . . . . . . . . 11
β’ β‘(πΉ β π») = (β‘π» β β‘πΉ) |
94 | 93 | imaeq1i 6015 |
. . . . . . . . . 10
β’ (β‘(πΉ β π») β (V β { 0 })) = ((β‘π» β β‘πΉ) β (V β { 0 })) |
95 | | imaco 6208 |
. . . . . . . . . 10
β’ ((β‘π» β β‘πΉ) β (V β { 0 })) = (β‘π» β (β‘πΉ β (V β { 0 }))) |
96 | 94, 95 | eqtri 2765 |
. . . . . . . . 9
β’ (β‘(πΉ β π») β (V β { 0 })) = (β‘π» β (β‘πΉ β (V β { 0 }))) |
97 | | rnco2 6210 |
. . . . . . . . 9
β’ ran
(β‘π» β π) = (β‘π» β ran π) |
98 | 92, 96, 97 | 3sstr4g 3994 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (β‘(πΉ β π») β (V β { 0 })) β ran (β‘π» β π)) |
99 | | f1oexrnex 7869 |
. . . . . . . . . . . . 13
β’ ((π»:πΆβ1-1-ontoβπ΄ β§ π΄ β π) β π» β V) |
100 | 6, 2, 99 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β π» β V) |
101 | | coexg 7871 |
. . . . . . . . . . . 12
β’ ((πΉ β V β§ π» β V) β (πΉ β π») β V) |
102 | 85, 100, 101 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΉ β π») β V) |
103 | | suppimacnv 8110 |
. . . . . . . . . . 11
β’ (((πΉ β π») β V β§ 0 β V) β ((πΉ β π») supp 0 ) = (β‘(πΉ β π») β (V β { 0 }))) |
104 | 102, 16, 103 | sylancl 587 |
. . . . . . . . . 10
β’ (π β ((πΉ β π») supp 0 ) = (β‘(πΉ β π») β (V β { 0 }))) |
105 | 104 | sseq1d 3980 |
. . . . . . . . 9
β’ (π β (((πΉ β π») supp 0 ) β ran (β‘π» β π) β (β‘(πΉ β π») β (V β { 0 })) β ran (β‘π» β π))) |
106 | 105 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (((πΉ β π») supp 0 ) β ran (β‘π» β π) β (β‘(πΉ β π») β (V β { 0 })) β ran (β‘π» β π))) |
107 | 98, 106 | mpbird 257 |
. . . . . . 7
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β ((πΉ β π») supp 0 ) β ran (β‘π» β π)) |
108 | | eqid 2737 |
. . . . . . 7
β’ (((πΉ β π») β (β‘π» β π)) supp 0 ) = (((πΉ β π») β (β‘π» β π)) supp 0 ) |
109 | 53, 3, 54, 55, 56, 70, 73, 77, 61, 83, 107, 108 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
(πΉ β π»)) =
(seq1((+gβπΊ), ((πΉ β π») β (β‘π» β π)))β(β―β(πΉ supp 0 )))) |
110 | 52, 69, 109 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ ((β―β(πΉ supp 0 )) β β β§
π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (πΉ β π»))) |
111 | 110 | expr 458 |
. . . 4
β’ ((π β§ (β―β(πΉ supp 0 )) β β) β
(π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (πΉ β π»)))) |
112 | 111 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―β(πΉ supp 0 )) β β) β
(βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (πΉ β π»)))) |
113 | 112 | expimpd 455 |
. 2
β’ (π β (((β―β(πΉ supp 0 )) β β β§
βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) β (πΊ Ξ£g
πΉ) = (πΊ Ξ£g (πΉ β π»)))) |
114 | | gsumzcl.w |
. . 3
β’ (π β πΉ finSupp 0 ) |
115 | | fsuppimp 9318 |
. . . 4
β’ (πΉ finSupp 0 β (Fun πΉ β§ (πΉ supp 0 ) β
Fin)) |
116 | 115 | simprd 497 |
. . 3
β’ (πΉ finSupp 0 β (πΉ supp 0 ) β
Fin) |
117 | | fz1f1o 15602 |
. . 3
β’ ((πΉ supp 0 ) β Fin β
((πΉ supp 0 ) = β
β¨
((β―β(πΉ supp
0 ))
β β β§ βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )))) |
118 | 114, 116,
117 | 3syl 18 |
. 2
β’ (π β ((πΉ supp 0 ) = β
β¨
((β―β(πΉ supp
0 ))
β β β§ βπ π:(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )))) |
119 | 30, 113, 118 | mpjaod 859 |
1
β’ (π β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (πΉ β π»))) |