Step | Hyp | Ref
| Expression |
1 | | gsumzoppg.g |
. . . . . . . 8
β’ (π β πΊ β Mnd) |
2 | | gsumzoppg.o |
. . . . . . . . 9
β’ π =
(oppgβπΊ) |
3 | 2 | oppgmnd 19142 |
. . . . . . . 8
β’ (πΊ β Mnd β π β Mnd) |
4 | 1, 3 | syl 17 |
. . . . . . 7
β’ (π β π β Mnd) |
5 | | gsumzoppg.a |
. . . . . . 7
β’ (π β π΄ β π) |
6 | | gsumzoppg.0 |
. . . . . . . . 9
β’ 0 =
(0gβπΊ) |
7 | 2, 6 | oppgid 19144 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
8 | 7 | gsumz 18653 |
. . . . . . 7
β’ ((π β Mnd β§ π΄ β π) β (π Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
9 | 4, 5, 8 | syl2anc 585 |
. . . . . 6
β’ (π β (π Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
10 | 6 | gsumz 18653 |
. . . . . . 7
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
11 | 1, 5, 10 | syl2anc 585 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
12 | 9, 11 | eqtr4d 2780 |
. . . . 5
β’ (π β (π Ξ£g (π β π΄ β¦ 0 )) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π
Ξ£g (π β π΄ β¦ 0 )) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
14 | | gsumzoppg.f |
. . . . . 6
β’ (π β πΉ:π΄βΆπ΅) |
15 | 6 | fvexi 6861 |
. . . . . . 7
β’ 0 β
V |
16 | 15 | a1i 11 |
. . . . . 6
β’ (π β 0 β V) |
17 | | ssid 3971 |
. . . . . . 7
β’ (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })) |
18 | 14, 5 | fexd 7182 |
. . . . . . . . 9
β’ (π β πΉ β V) |
19 | | suppimacnv 8110 |
. . . . . . . . 9
β’ ((πΉ β V β§ 0 β V)
β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
20 | 18, 15, 19 | sylancl 587 |
. . . . . . . 8
β’ (π β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
21 | 20 | sseq1d 3980 |
. . . . . . 7
β’ (π β ((πΉ supp 0 ) β (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })))) |
22 | 17, 21 | mpbiri 258 |
. . . . . 6
β’ (π β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
23 | 14, 5, 16, 22 | gsumcllem 19692 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
πΉ = (π β π΄ β¦ 0 )) |
24 | 23 | oveq2d 7378 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π
Ξ£g πΉ) = (π Ξ£g (π β π΄ β¦ 0 ))) |
25 | 23 | oveq2d 7378 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g πΉ) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
26 | 13, 24, 25 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π
Ξ£g πΉ) = (πΊ Ξ£g πΉ)) |
27 | 26 | ex 414 |
. 2
β’ (π β ((β‘πΉ β (V β { 0 })) = β
β
(π
Ξ£g πΉ) = (πΊ Ξ£g πΉ))) |
28 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(β―β(β‘πΉ β (V β { 0 }))) β
β) |
29 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
30 | 28, 29 | eleqtrdi 2848 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(β―β(β‘πΉ β (V β { 0 }))) β
(β€β₯β1)) |
31 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΉ:π΄βΆπ΅) |
32 | | ffn 6673 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
33 | | dffn4 6767 |
. . . . . . . . . . . 12
β’ (πΉ Fn π΄ β πΉ:π΄βontoβran πΉ) |
34 | 32, 33 | sylib 217 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βontoβran πΉ) |
35 | | fof 6761 |
. . . . . . . . . . 11
β’ (πΉ:π΄βontoβran πΉ β πΉ:π΄βΆran πΉ) |
36 | 31, 34, 35 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΉ:π΄βΆran πΉ) |
37 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΊ β Mnd) |
38 | | gsumzoppg.b |
. . . . . . . . . . . . 13
β’ π΅ = (BaseβπΊ) |
39 | 38 | submacs 18644 |
. . . . . . . . . . . 12
β’ (πΊ β Mnd β
(SubMndβπΊ) β
(ACSβπ΅)) |
40 | | acsmre 17539 |
. . . . . . . . . . . 12
β’
((SubMndβπΊ)
β (ACSβπ΅) β
(SubMndβπΊ) β
(Mooreβπ΅)) |
41 | 37, 39, 40 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(SubMndβπΊ) β
(Mooreβπ΅)) |
42 | | eqid 2737 |
. . . . . . . . . . 11
β’
(mrClsβ(SubMndβπΊ)) = (mrClsβ(SubMndβπΊ)) |
43 | 31 | frnd 6681 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran πΉ β π΅) |
44 | 41, 42, 43 | mrcssidd 17512 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran πΉ β
((mrClsβ(SubMndβπΊ))βran πΉ)) |
45 | 36, 44 | fssd 6691 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΉ:π΄βΆ((mrClsβ(SubMndβπΊ))βran πΉ)) |
46 | | f1of1 6788 |
. . . . . . . . . . . 12
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0
}))) |
47 | 46 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0
}))) |
48 | | cnvimass 6038 |
. . . . . . . . . . . 12
β’ (β‘πΉ β (V β { 0 })) β dom πΉ |
49 | 48, 31 | fssdm 6693 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (β‘πΉ β (V β { 0 })) β π΄) |
50 | | f1ss 6749 |
. . . . . . . . . . 11
β’ ((π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0 })) β§
(β‘πΉ β (V β { 0 })) β π΄) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
51 | 47, 49, 50 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
52 | | f1f 6743 |
. . . . . . . . . 10
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄ β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) |
54 | | fco 6697 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆ((mrClsβ(SubMndβπΊ))βran πΉ) β§ π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) β (πΉ β π):(1...(β―β(β‘πΉ β (V β { 0
}))))βΆ((mrClsβ(SubMndβπΊ))βran πΉ)) |
55 | 45, 53, 54 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ β π):(1...(β―β(β‘πΉ β (V β { 0
}))))βΆ((mrClsβ(SubMndβπΊ))βran πΉ)) |
56 | 55 | ffvelcdmda 7040 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΉ β π)βπ₯) β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
57 | 42 | mrccl 17498 |
. . . . . . . . . 10
β’
(((SubMndβπΊ)
β (Mooreβπ΅)
β§ ran πΉ β π΅) β
((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ)) |
58 | 41, 43, 57 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ)) |
59 | 2 | oppgsubm 19150 |
. . . . . . . . 9
β’
(SubMndβπΊ) =
(SubMndβπ) |
60 | 58, 59 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπ)) |
61 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
62 | 61 | submcl 18630 |
. . . . . . . . 9
β’
((((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπ) β§ π₯ β ((mrClsβ(SubMndβπΊ))βran πΉ) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ)) β (π₯(+gβπ)π¦) β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
63 | 62 | 3expb 1121 |
. . . . . . . 8
β’
((((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπ) β§ (π₯ β ((mrClsβ(SubMndβπΊ))βran πΉ) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ))) β (π₯(+gβπ)π¦) β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
64 | 60, 63 | sylan 581 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ (π₯ β
((mrClsβ(SubMndβπΊ))βran πΉ) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ))) β (π₯(+gβπ)π¦) β ((mrClsβ(SubMndβπΊ))βran πΉ)) |
65 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
66 | 65, 2, 61 | oppgplus 19134 |
. . . . . . . . 9
β’ (π₯(+gβπ)π¦) = (π¦(+gβπΊ)π₯) |
67 | | gsumzoppg.c |
. . . . . . . . . . . . . 14
β’ (π β ran πΉ β (πβran πΉ)) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran πΉ β (πβran πΉ)) |
69 | | gsumzoppg.z |
. . . . . . . . . . . . . 14
β’ π = (CntzβπΊ) |
70 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) = (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) |
71 | 69, 42, 70 | cntzspan 19629 |
. . . . . . . . . . . . 13
β’ ((πΊ β Mnd β§ ran πΉ β (πβran πΉ)) β (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd) |
72 | 37, 68, 71 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd) |
73 | 70, 69 | submcmn2 19624 |
. . . . . . . . . . . . 13
β’
(((mrClsβ(SubMndβπΊ))βran πΉ) β (SubMndβπΊ) β ((πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd β
((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)))) |
74 | 58, 73 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΊ βΎs
((mrClsβ(SubMndβπΊ))βran πΉ)) β CMnd β
((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)))) |
75 | 72, 74 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
((mrClsβ(SubMndβπΊ))βran πΉ) β (πβ((mrClsβ(SubMndβπΊ))βran πΉ))) |
76 | 75 | sselda 3949 |
. . . . . . . . . 10
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
((mrClsβ(SubMndβπΊ))βran πΉ)) β π₯ β (πβ((mrClsβ(SubMndβπΊ))βran πΉ))) |
77 | 65, 69 | cntzi 19116 |
. . . . . . . . . 10
β’ ((π₯ β (πβ((mrClsβ(SubMndβπΊ))βran πΉ)) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ)) β (π₯(+gβπΊ)π¦) = (π¦(+gβπΊ)π₯)) |
78 | 76, 77 | sylan 581 |
. . . . . . . . 9
β’ ((((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
((mrClsβ(SubMndβπΊ))βran πΉ)) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ)) β (π₯(+gβπΊ)π¦) = (π¦(+gβπΊ)π₯)) |
79 | 66, 78 | eqtr4id 2796 |
. . . . . . . 8
β’ ((((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
((mrClsβ(SubMndβπΊ))βran πΉ)) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ)) β (π₯(+gβπ)π¦) = (π₯(+gβπΊ)π¦)) |
80 | 79 | anasss 468 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ (π₯ β
((mrClsβ(SubMndβπΊ))βran πΉ) β§ π¦ β ((mrClsβ(SubMndβπΊ))βran πΉ))) β (π₯(+gβπ)π¦) = (π₯(+gβπΊ)π¦)) |
81 | 30, 56, 64, 80 | seqfeq4 13964 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(seq1((+gβπ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 })))) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
82 | 2, 38 | oppgbas 19137 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
83 | | eqid 2737 |
. . . . . . 7
β’
(Cntzβπ) =
(Cntzβπ) |
84 | 37, 3 | syl 17 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π β Mnd) |
85 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π΄ β π) |
86 | 2, 69 | oppgcntz 19152 |
. . . . . . . 8
β’ (πβran πΉ) = ((Cntzβπ)βran πΉ) |
87 | 68, 86 | sseqtrdi 3999 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran πΉ β ((Cntzβπ)βran πΉ)) |
88 | | suppssdm 8113 |
. . . . . . . . . . 11
β’ (πΉ supp 0 ) β dom πΉ |
89 | 20, 88 | eqsstrrdi 4004 |
. . . . . . . . . 10
β’ (π β (β‘πΉ β (V β { 0 })) β dom πΉ) |
90 | 14, 89 | fssdmd 6692 |
. . . . . . . . 9
β’ (π β (β‘πΉ β (V β { 0 })) β π΄) |
91 | 90 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (β‘πΉ β (V β { 0 })) β π΄) |
92 | 47, 91, 50 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
93 | 21 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΉ supp 0 ) β (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })))) |
94 | 17, 93 | mpbiri 258 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
95 | | f1ofo 6796 |
. . . . . . . . . . 11
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βontoβ(β‘πΉ β (V β { 0 }))) |
96 | | forn 6764 |
. . . . . . . . . . 11
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))βontoβ(β‘πΉ β (V β { 0 })) β ran π = (β‘πΉ β (V β { 0 }))) |
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β ran π = (β‘πΉ β (V β { 0 }))) |
98 | 97 | sseq2d 3981 |
. . . . . . . . 9
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β ((πΉ supp 0 ) β ran π β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 })))) |
99 | 98 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΉ supp 0 ) β ran π β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 })))) |
100 | 94, 99 | mpbird 257 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β ran π) |
101 | | eqid 2737 |
. . . . . . 7
β’ ((πΉ β π) supp 0 ) = ((πΉ β π) supp 0 ) |
102 | 82, 7, 61, 83, 84, 85, 31, 87, 28, 92, 100, 101 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (π Ξ£g
πΉ) =
(seq1((+gβπ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
103 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
104 | 103, 99 | mpbird 257 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β ran π) |
105 | 38, 6, 65, 69, 37, 85, 31, 68, 28, 92, 104, 101 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΊ Ξ£g
πΉ) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
106 | 81, 102, 105 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (π Ξ£g
πΉ) = (πΊ Ξ£g πΉ)) |
107 | 106 | expr 458 |
. . . 4
β’ ((π β§ (β―β(β‘πΉ β (V β { 0 }))) β β)
β (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β (π Ξ£g
πΉ) = (πΊ Ξ£g πΉ))) |
108 | 107 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―β(β‘πΉ β (V β { 0 }))) β β)
β (βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β (π Ξ£g
πΉ) = (πΊ Ξ£g πΉ))) |
109 | 108 | expimpd 455 |
. 2
β’ (π β (((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))) β (π Ξ£g
πΉ) = (πΊ Ξ£g πΉ))) |
110 | | gsumzoppg.n |
. . . . 5
β’ (π β πΉ finSupp 0 ) |
111 | 110 | fsuppimpd 9319 |
. . . 4
β’ (π β (πΉ supp 0 ) β
Fin) |
112 | 20, 111 | eqeltrrd 2839 |
. . 3
β’ (π β (β‘πΉ β (V β { 0 })) β
Fin) |
113 | | fz1f1o 15602 |
. . 3
β’ ((β‘πΉ β (V β { 0 })) β Fin β
((β‘πΉ β (V β { 0 })) = β
β¨
((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))))) |
114 | 112, 113 | syl 17 |
. 2
β’ (π β ((β‘πΉ β (V β { 0 })) = β
β¨
((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))))) |
115 | 27, 109, 114 | mpjaod 859 |
1
β’ (π β (π Ξ£g πΉ) = (πΊ Ξ£g πΉ)) |