Step | Hyp | Ref
| Expression |
1 | | gsumzmhm.h |
. . . . . . 7
β’ (π β π» β Mnd) |
2 | | gsumzmhm.a |
. . . . . . 7
β’ (π β π΄ β π) |
3 | | eqid 2737 |
. . . . . . . 8
β’
(0gβπ») = (0gβπ») |
4 | 3 | gsumz 18653 |
. . . . . . 7
β’ ((π» β Mnd β§ π΄ β π) β (π» Ξ£g (π β π΄ β¦ (0gβπ»))) = (0gβπ»)) |
5 | 1, 2, 4 | syl2anc 585 |
. . . . . 6
β’ (π β (π» Ξ£g (π β π΄ β¦ (0gβπ»))) = (0gβπ»)) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (π β π΄ β¦ (0gβπ»))) = (0gβπ»)) |
7 | | gsumzmhm.k |
. . . . . . 7
β’ (π β πΎ β (πΊ MndHom π»)) |
8 | | gsumzmhm.0 |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
9 | 8, 3 | mhm0 18617 |
. . . . . . 7
β’ (πΎ β (πΊ MndHom π») β (πΎβ 0 ) =
(0gβπ»)) |
10 | 7, 9 | syl 17 |
. . . . . 6
β’ (π β (πΎβ 0 ) =
(0gβπ»)) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎβ 0 ) =
(0gβπ»)) |
12 | 6, 11 | eqtr4d 2780 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (π β π΄ β¦ (0gβπ»))) = (πΎβ 0 )) |
13 | | gsumzmhm.g |
. . . . . . . . 9
β’ (π β πΊ β Mnd) |
14 | | gsumzmhm.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
15 | 14, 8 | mndidcl 18578 |
. . . . . . . . 9
β’ (πΊ β Mnd β 0 β π΅) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
β’ (π β 0 β π΅) |
17 | 16 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (β‘πΉ β (V β { 0 })) = β
) β§ π β π΄) β 0 β π΅) |
18 | | gsumzmhm.f |
. . . . . . . 8
β’ (π β πΉ:π΄βΆπ΅) |
19 | 8 | fvexi 6861 |
. . . . . . . . 9
β’ 0 β
V |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β V) |
21 | 18, 2 | fexd 7182 |
. . . . . . . . . 10
β’ (π β πΉ β V) |
22 | | suppimacnv 8110 |
. . . . . . . . . 10
β’ ((πΉ β V β§ 0 β V)
β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
23 | 21, 20, 22 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
24 | | ssid 3971 |
. . . . . . . . 9
β’ (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })) |
25 | 23, 24 | eqsstrdi 4003 |
. . . . . . . 8
β’ (π β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
26 | 18, 2, 20, 25 | gsumcllem 19692 |
. . . . . . 7
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
πΉ = (π β π΄ β¦ 0 )) |
27 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ») =
(Baseβπ») |
28 | 14, 27 | mhmf 18614 |
. . . . . . . . . 10
β’ (πΎ β (πΊ MndHom π») β πΎ:π΅βΆ(Baseβπ»)) |
29 | 7, 28 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ:π΅βΆ(Baseβπ»)) |
30 | 29 | feqmptd 6915 |
. . . . . . . 8
β’ (π β πΎ = (π₯ β π΅ β¦ (πΎβπ₯))) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
πΎ = (π₯ β π΅ β¦ (πΎβπ₯))) |
32 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = 0 β (πΎβπ₯) = (πΎβ 0 )) |
33 | 17, 26, 31, 32 | fmptco 7080 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎ β πΉ) = (π β π΄ β¦ (πΎβ 0 ))) |
34 | 10 | mpteq2dv 5212 |
. . . . . . 7
β’ (π β (π β π΄ β¦ (πΎβ 0 )) = (π β π΄ β¦ (0gβπ»))) |
35 | 34 | adantr 482 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π β π΄ β¦ (πΎβ 0 )) = (π β π΄ β¦ (0gβπ»))) |
36 | 33, 35 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎ β πΉ) = (π β π΄ β¦ (0gβπ»))) |
37 | 36 | oveq2d 7378 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (πΎ β πΉ)) = (π» Ξ£g (π β π΄ β¦ (0gβπ»)))) |
38 | 26 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g πΉ) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
39 | 8 | gsumz 18653 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
40 | 13, 2, 39 | syl2anc 585 |
. . . . . . 7
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
41 | 40 | adantr 482 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
42 | 38, 41 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g πΉ) = 0 ) |
43 | 42 | fveq2d 6851 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎβ(πΊ Ξ£g πΉ)) = (πΎβ 0 )) |
44 | 12, 37, 43 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) |
45 | 44 | ex 414 |
. 2
β’ (π β ((β‘πΉ β (V β { 0 })) = β
β
(π»
Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
46 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΊ β Mnd) |
47 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
48 | 14, 47 | mndcl 18571 |
. . . . . . . . 9
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπΊ)π¦) β π΅) |
49 | 48 | 3expb 1121 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) β π΅) |
50 | 46, 49 | sylan 581 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) β π΅) |
51 | | f1of1 6788 |
. . . . . . . . . . . 12
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0
}))) |
52 | 51 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0
}))) |
53 | | cnvimass 6038 |
. . . . . . . . . . . 12
β’ (β‘πΉ β (V β { 0 })) β dom πΉ |
54 | 18 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΉ:π΄βΆπ΅) |
55 | 53, 54 | fssdm 6693 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (β‘πΉ β (V β { 0 })) β π΄) |
56 | | f1ss 6749 |
. . . . . . . . . . 11
β’ ((π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0 })) β§
(β‘πΉ β (V β { 0 })) β π΄) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
57 | 52, 55, 56 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
58 | | f1f 6743 |
. . . . . . . . . 10
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄ β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) |
60 | | fco 6697 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) β (πΉ β π):(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΅) |
61 | 18, 59, 60 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ β π):(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΅) |
62 | 61 | ffvelcdmda 7040 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΉ β π)βπ₯) β π΅) |
63 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(β―β(β‘πΉ β (V β { 0 }))) β
β) |
64 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
65 | 63, 64 | eleqtrdi 2848 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(β―β(β‘πΉ β (V β { 0 }))) β
(β€β₯β1)) |
66 | 7 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΎ β (πΊ MndHom π»)) |
67 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπ») = (+gβπ») |
68 | 14, 47, 67 | mhmlin 18616 |
. . . . . . . . 9
β’ ((πΎ β (πΊ MndHom π») β§ π₯ β π΅ β§ π¦ β π΅) β (πΎβ(π₯(+gβπΊ)π¦)) = ((πΎβπ₯)(+gβπ»)(πΎβπ¦))) |
69 | 68 | 3expb 1121 |
. . . . . . . 8
β’ ((πΎ β (πΊ MndHom π») β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΎβ(π₯(+gβπΊ)π¦)) = ((πΎβπ₯)(+gβπ»)(πΎβπ¦))) |
70 | 66, 69 | sylan 581 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΎβ(π₯(+gβπΊ)π¦)) = ((πΎβπ₯)(+gβπ»)(πΎβπ¦))) |
71 | | coass 6222 |
. . . . . . . . 9
β’ ((πΎ β πΉ) β π) = (πΎ β (πΉ β π)) |
72 | 71 | fveq1i 6848 |
. . . . . . . 8
β’ (((πΎ β πΉ) β π)βπ₯) = ((πΎ β (πΉ β π))βπ₯) |
73 | | fvco3 6945 |
. . . . . . . . 9
β’ (((πΉ β π):(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΅ β§ π₯ β (1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΎ β (πΉ β π))βπ₯) = (πΎβ((πΉ β π)βπ₯))) |
74 | 61, 73 | sylan 581 |
. . . . . . . 8
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΎ β (πΉ β π))βπ₯) = (πΎβ((πΉ β π)βπ₯))) |
75 | 72, 74 | eqtr2id 2790 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β (πΎβ((πΉ β π)βπ₯)) = (((πΎ β πΉ) β π)βπ₯)) |
76 | 50, 62, 65, 70, 75 | seqhomo 13962 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎβ(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 }))))) =
(seq1((+gβπ»), ((πΎ β πΉ) β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
77 | | gsumzmhm.z |
. . . . . . . 8
β’ π = (CntzβπΊ) |
78 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π΄ β π) |
79 | | gsumzmhm.c |
. . . . . . . . 9
β’ (π β ran πΉ β (πβran πΉ)) |
80 | 79 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran πΉ β (πβran πΉ)) |
81 | 25 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
82 | | f1ofo 6796 |
. . . . . . . . . . 11
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βontoβ(β‘πΉ β (V β { 0 }))) |
83 | | forn 6764 |
. . . . . . . . . . 11
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))βontoβ(β‘πΉ β (V β { 0 })) β ran π = (β‘πΉ β (V β { 0 }))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . 10
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β ran π = (β‘πΉ β (V β { 0 }))) |
85 | 84 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran π = (β‘πΉ β (V β { 0 }))) |
86 | 81, 85 | sseqtrrd 3990 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β ran π) |
87 | | eqid 2737 |
. . . . . . . 8
β’ ((πΉ β π) supp 0 ) = ((πΉ β π) supp 0 ) |
88 | 14, 8, 47, 77, 46, 78, 54, 80, 63, 57, 86, 87 | gsumval3 19691 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΊ Ξ£g
πΉ) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
89 | 88 | fveq2d 6851 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎβ(πΊ Ξ£g πΉ)) = (πΎβ(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 })))))) |
90 | | eqid 2737 |
. . . . . . 7
β’
(Cntzβπ») =
(Cntzβπ») |
91 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π» β Mnd) |
92 | | fco 6697 |
. . . . . . . 8
β’ ((πΎ:π΅βΆ(Baseβπ») β§ πΉ:π΄βΆπ΅) β (πΎ β πΉ):π΄βΆ(Baseβπ»)) |
93 | 29, 54, 92 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎ β πΉ):π΄βΆ(Baseβπ»)) |
94 | 77, 90 | cntzmhm2 19127 |
. . . . . . . . 9
β’ ((πΎ β (πΊ MndHom π») β§ ran πΉ β (πβran πΉ)) β (πΎ β ran πΉ) β ((Cntzβπ»)β(πΎ β ran πΉ))) |
95 | 7, 80, 94 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎ β ran πΉ) β ((Cntzβπ»)β(πΎ β ran πΉ))) |
96 | | rnco2 6210 |
. . . . . . . 8
β’ ran
(πΎ β πΉ) = (πΎ β ran πΉ) |
97 | 96 | fveq2i 6850 |
. . . . . . . 8
β’
((Cntzβπ»)βran (πΎ β πΉ)) = ((Cntzβπ»)β(πΎ β ran πΉ)) |
98 | 95, 96, 97 | 3sstr4g 3994 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran (πΎ β πΉ) β ((Cntzβπ»)βran (πΎ β πΉ))) |
99 | | eldifi 4091 |
. . . . . . . . . . 11
β’ (π₯ β (π΄ β (β‘πΉ β (V β { 0 }))) β π₯ β π΄) |
100 | | fvco3 6945 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆπ΅ β§ π₯ β π΄) β ((πΎ β πΉ)βπ₯) = (πΎβ(πΉβπ₯))) |
101 | 54, 99, 100 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ)βπ₯) = (πΎβ(πΉβπ₯))) |
102 | 19 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β 0 β
V) |
103 | 54, 81, 78, 102 | suppssr 8132 |
. . . . . . . . . . 11
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β (πΉβπ₯) = 0 ) |
104 | 103 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β (πΎβ(πΉβπ₯)) = (πΎβ 0 )) |
105 | 10 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β (πΎβ 0 ) =
(0gβπ»)) |
106 | 101, 104,
105 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ)βπ₯) = (0gβπ»)) |
107 | 93, 106 | suppss 8130 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ) supp (0gβπ»)) β (β‘πΉ β (V β { 0 }))) |
108 | 107, 85 | sseqtrrd 3990 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ) supp (0gβπ»)) β ran π) |
109 | | eqid 2737 |
. . . . . . 7
β’ (((πΎ β πΉ) β π) supp (0gβπ»)) = (((πΎ β πΉ) β π) supp (0gβπ»)) |
110 | 27, 3, 67, 90, 91, 78, 93, 98, 63, 57, 108, 109 | gsumval3 19691 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (π» Ξ£g
(πΎ β πΉ)) =
(seq1((+gβπ»), ((πΎ β πΉ) β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
111 | 76, 89, 110 | 3eqtr4rd 2788 |
. . . . 5
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) |
112 | 111 | expr 458 |
. . . 4
β’ ((π β§ (β―β(β‘πΉ β (V β { 0 }))) β β)
β (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
113 | 112 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―β(β‘πΉ β (V β { 0 }))) β β)
β (βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
114 | 113 | expimpd 455 |
. 2
β’ (π β (((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
115 | | gsumzmhm.w |
. . . . 5
β’ (π β πΉ finSupp 0 ) |
116 | 115 | fsuppimpd 9319 |
. . . 4
β’ (π β (πΉ supp 0 ) β
Fin) |
117 | 23, 116 | eqeltrrd 2839 |
. . 3
β’ (π β (β‘πΉ β (V β { 0 })) β
Fin) |
118 | | fz1f1o 15602 |
. . 3
β’ ((β‘πΉ β (V β { 0 })) β Fin β
((β‘πΉ β (V β { 0 })) = β
β¨
((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))))) |
119 | 117, 118 | syl 17 |
. 2
β’ (π β ((β‘πΉ β (V β { 0 })) = β
β¨
((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))))) |
120 | 45, 114, 119 | mpjaod 859 |
1
β’ (π β (π» Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) |