Step | Hyp | Ref
| Expression |
1 | | gsumzmhm.h |
. . . . . . 7
β’ (π β π» β Mnd) |
2 | | gsumzmhm.a |
. . . . . . 7
β’ (π β π΄ β π) |
3 | | eqid 2732 |
. . . . . . . 8
β’
(0gβπ») = (0gβπ») |
4 | 3 | gsumz 18713 |
. . . . . . 7
β’ ((π» β Mnd β§ π΄ β π) β (π» Ξ£g (π β π΄ β¦ (0gβπ»))) = (0gβπ»)) |
5 | 1, 2, 4 | syl2anc 584 |
. . . . . 6
β’ (π β (π» Ξ£g (π β π΄ β¦ (0gβπ»))) = (0gβπ»)) |
6 | 5 | adantr 481 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (π β π΄ β¦ (0gβπ»))) = (0gβπ»)) |
7 | | gsumzmhm.k |
. . . . . . 7
β’ (π β πΎ β (πΊ MndHom π»)) |
8 | | gsumzmhm.0 |
. . . . . . . 8
β’ 0 =
(0gβπΊ) |
9 | 8, 3 | mhm0 18676 |
. . . . . . 7
β’ (πΎ β (πΊ MndHom π») β (πΎβ 0 ) =
(0gβπ»)) |
10 | 7, 9 | syl 17 |
. . . . . 6
β’ (π β (πΎβ 0 ) =
(0gβπ»)) |
11 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎβ 0 ) =
(0gβπ»)) |
12 | 6, 11 | eqtr4d 2775 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (π β π΄ β¦ (0gβπ»))) = (πΎβ 0 )) |
13 | | gsumzmhm.g |
. . . . . . . . 9
β’ (π β πΊ β Mnd) |
14 | | gsumzmhm.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΊ) |
15 | 14, 8 | mndidcl 18636 |
. . . . . . . . 9
β’ (πΊ β Mnd β 0 β π΅) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
β’ (π β 0 β π΅) |
17 | 16 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ (β‘πΉ β (V β { 0 })) = β
) β§ π β π΄) β 0 β π΅) |
18 | | gsumzmhm.f |
. . . . . . . 8
β’ (π β πΉ:π΄βΆπ΅) |
19 | 8 | fvexi 6902 |
. . . . . . . . 9
β’ 0 β
V |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β V) |
21 | 18, 2 | fexd 7225 |
. . . . . . . . . 10
β’ (π β πΉ β V) |
22 | | suppimacnv 8155 |
. . . . . . . . . 10
β’ ((πΉ β V β§ 0 β V)
β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
23 | 21, 20, 22 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (πΉ supp 0 ) = (β‘πΉ β (V β { 0 }))) |
24 | | ssid 4003 |
. . . . . . . . 9
β’ (β‘πΉ β (V β { 0 })) β (β‘πΉ β (V β { 0 })) |
25 | 23, 24 | eqsstrdi 4035 |
. . . . . . . 8
β’ (π β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
26 | 18, 2, 20, 25 | gsumcllem 19770 |
. . . . . . 7
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
πΉ = (π β π΄ β¦ 0 )) |
27 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβπ») =
(Baseβπ») |
28 | 14, 27 | mhmf 18673 |
. . . . . . . . . 10
β’ (πΎ β (πΊ MndHom π») β πΎ:π΅βΆ(Baseβπ»)) |
29 | 7, 28 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ:π΅βΆ(Baseβπ»)) |
30 | 29 | feqmptd 6957 |
. . . . . . . 8
β’ (π β πΎ = (π₯ β π΅ β¦ (πΎβπ₯))) |
31 | 30 | adantr 481 |
. . . . . . 7
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
πΎ = (π₯ β π΅ β¦ (πΎβπ₯))) |
32 | | fveq2 6888 |
. . . . . . 7
β’ (π₯ = 0 β (πΎβπ₯) = (πΎβ 0 )) |
33 | 17, 26, 31, 32 | fmptco 7123 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎ β πΉ) = (π β π΄ β¦ (πΎβ 0 ))) |
34 | 10 | mpteq2dv 5249 |
. . . . . . 7
β’ (π β (π β π΄ β¦ (πΎβ 0 )) = (π β π΄ β¦ (0gβπ»))) |
35 | 34 | adantr 481 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π β π΄ β¦ (πΎβ 0 )) = (π β π΄ β¦ (0gβπ»))) |
36 | 33, 35 | eqtrd 2772 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎ β πΉ) = (π β π΄ β¦ (0gβπ»))) |
37 | 36 | oveq2d 7421 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (πΎ β πΉ)) = (π» Ξ£g (π β π΄ β¦ (0gβπ»)))) |
38 | 26 | oveq2d 7421 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g πΉ) = (πΊ Ξ£g (π β π΄ β¦ 0 ))) |
39 | 8 | gsumz 18713 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
40 | 13, 2, 39 | syl2anc 584 |
. . . . . . 7
β’ (π β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
41 | 40 | adantr 481 |
. . . . . 6
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g (π β π΄ β¦ 0 )) = 0 ) |
42 | 38, 41 | eqtrd 2772 |
. . . . 5
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΊ
Ξ£g πΉ) = 0 ) |
43 | 42 | fveq2d 6892 |
. . . 4
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(πΎβ(πΊ Ξ£g πΉ)) = (πΎβ 0 )) |
44 | 12, 37, 43 | 3eqtr4d 2782 |
. . 3
β’ ((π β§ (β‘πΉ β (V β { 0 })) = β
) β
(π»
Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) |
45 | 44 | ex 413 |
. 2
β’ (π β ((β‘πΉ β (V β { 0 })) = β
β
(π»
Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
46 | 13 | adantr 481 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΊ β Mnd) |
47 | | eqid 2732 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
48 | 14, 47 | mndcl 18629 |
. . . . . . . . 9
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπΊ)π¦) β π΅) |
49 | 48 | 3expb 1120 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) β π΅) |
50 | 46, 49 | sylan 580 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) β π΅) |
51 | | f1of1 6829 |
. . . . . . . . . . . 12
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0
}))) |
52 | 51 | ad2antll 727 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0
}))) |
53 | | cnvimass 6077 |
. . . . . . . . . . . 12
β’ (β‘πΉ β (V β { 0 })) β dom πΉ |
54 | 18 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΉ:π΄βΆπ΅) |
55 | 53, 54 | fssdm 6734 |
. . . . . . . . . . 11
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (β‘πΉ β (V β { 0 })) β π΄) |
56 | | f1ss 6790 |
. . . . . . . . . . 11
β’ ((π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1β(β‘πΉ β (V β { 0 })) β§
(β‘πΉ β (V β { 0 })) β π΄) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
57 | 52, 55, 56 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1βπ΄) |
58 | | f1f 6784 |
. . . . . . . . . 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 6738 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π:(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΄) β (πΉ β π):(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΅) |
61 | 18, 59, 60 | syl2an2r 683 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ β π):(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΅) |
62 | 61 | ffvelcdmda 7083 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΉ β π)βπ₯) β π΅) |
63 | | simprl 769 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(β―β(β‘πΉ β (V β { 0 }))) β
β) |
64 | | nnuz 12861 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
65 | 63, 64 | eleqtrdi 2843 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β
(β―β(β‘πΉ β (V β { 0 }))) β
(β€β₯β1)) |
66 | 7 | adantr 481 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β πΎ β (πΊ MndHom π»)) |
67 | | eqid 2732 |
. . . . . . . . . 10
β’
(+gβπ») = (+gβπ») |
68 | 14, 47, 67 | mhmlin 18675 |
. . . . . . . . 9
β’ ((πΎ β (πΊ MndHom π») β§ π₯ β π΅ β§ π¦ β π΅) β (πΎβ(π₯(+gβπΊ)π¦)) = ((πΎβπ₯)(+gβπ»)(πΎβπ¦))) |
69 | 68 | 3expb 1120 |
. . . . . . . 8
β’ ((πΎ β (πΊ MndHom π») β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΎβ(π₯(+gβπΊ)π¦)) = ((πΎβπ₯)(+gβπ»)(πΎβπ¦))) |
70 | 66, 69 | sylan 580 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΎβ(π₯(+gβπΊ)π¦)) = ((πΎβπ₯)(+gβπ»)(πΎβπ¦))) |
71 | | coass 6261 |
. . . . . . . . 9
β’ ((πΎ β πΉ) β π) = (πΎ β (πΉ β π)) |
72 | 71 | fveq1i 6889 |
. . . . . . . 8
β’ (((πΎ β πΉ) β π)βπ₯) = ((πΎ β (πΉ β π))βπ₯) |
73 | | fvco3 6987 |
. . . . . . . . 9
β’ (((πΉ β π):(1...(β―β(β‘πΉ β (V β { 0 }))))βΆπ΅ β§ π₯ β (1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΎ β (πΉ β π))βπ₯) = (πΎβ((πΉ β π)βπ₯))) |
74 | 61, 73 | sylan 580 |
. . . . . . . 8
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β ((πΎ β (πΉ β π))βπ₯) = (πΎβ((πΉ β π)βπ₯))) |
75 | 72, 74 | eqtr2id 2785 |
. . . . . . 7
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β
(1...(β―β(β‘πΉ β (V β { 0 }))))) β (πΎβ((πΉ β π)βπ₯)) = (((πΎ β πΉ) β π)βπ₯)) |
76 | 50, 62, 65, 70, 75 | seqhomo 14011 |
. . . . . 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 481 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π΄ β π) |
79 | | gsumzmhm.c |
. . . . . . . . 9
β’ (π β ran πΉ β (πβran πΉ)) |
80 | 79 | adantr 481 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran πΉ β (πβran πΉ)) |
81 | 25 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β (β‘πΉ β (V β { 0 }))) |
82 | | f1ofo 6837 |
. . . . . . . . . . 11
β’ (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β π:(1...(β―β(β‘πΉ β (V β { 0 }))))βontoβ(β‘πΉ β (V β { 0 }))) |
83 | | forn 6805 |
. . . . . . . . . . 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 727 |
. . . . . . . . 9
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran π = (β‘πΉ β (V β { 0 }))) |
86 | 81, 85 | sseqtrrd 4022 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΉ supp 0 ) β ran π) |
87 | | eqid 2732 |
. . . . . . . 8
β’ ((πΉ β π) supp 0 ) = ((πΉ β π) supp 0 ) |
88 | 14, 8, 47, 77, 46, 78, 54, 80, 63, 57, 86, 87 | gsumval3 19769 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΊ Ξ£g
πΉ) =
(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
89 | 88 | fveq2d 6892 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎβ(πΊ Ξ£g πΉ)) = (πΎβ(seq1((+gβπΊ), (πΉ β π))β(β―β(β‘πΉ β (V β { 0 })))))) |
90 | | eqid 2732 |
. . . . . . 7
β’
(Cntzβπ») =
(Cntzβπ») |
91 | 1 | adantr 481 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β π» β Mnd) |
92 | | fco 6738 |
. . . . . . . 8
β’ ((πΎ:π΅βΆ(Baseβπ») β§ πΉ:π΄βΆπ΅) β (πΎ β πΉ):π΄βΆ(Baseβπ»)) |
93 | 29, 54, 92 | syl2an2r 683 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎ β πΉ):π΄βΆ(Baseβπ»)) |
94 | 77, 90 | cntzmhm2 19200 |
. . . . . . . . 9
β’ ((πΎ β (πΊ MndHom π») β§ ran πΉ β (πβran πΉ)) β (πΎ β ran πΉ) β ((Cntzβπ»)β(πΎ β ran πΉ))) |
95 | 7, 80, 94 | syl2an2r 683 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (πΎ β ran πΉ) β ((Cntzβπ»)β(πΎ β ran πΉ))) |
96 | | rnco2 6249 |
. . . . . . . 8
β’ ran
(πΎ β πΉ) = (πΎ β ran πΉ) |
97 | 96 | fveq2i 6891 |
. . . . . . . 8
β’
((Cntzβπ»)βran (πΎ β πΉ)) = ((Cntzβπ»)β(πΎ β ran πΉ)) |
98 | 95, 96, 97 | 3sstr4g 4026 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ran (πΎ β πΉ) β ((Cntzβπ»)βran (πΎ β πΉ))) |
99 | | eldifi 4125 |
. . . . . . . . . . 11
β’ (π₯ β (π΄ β (β‘πΉ β (V β { 0 }))) β π₯ β π΄) |
100 | | fvco3 6987 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆπ΅ β§ π₯ β π΄) β ((πΎ β πΉ)βπ₯) = (πΎβ(πΉβπ₯))) |
101 | 54, 99, 100 | syl2an 596 |
. . . . . . . . . 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 8177 |
. . . . . . . . . . 11
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β (πΉβπ₯) = 0 ) |
104 | 103 | fveq2d 6892 |
. . . . . . . . . 10
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β (πΎβ(πΉβπ₯)) = (πΎβ 0 )) |
105 | 10 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β (πΎβ 0 ) =
(0gβπ»)) |
106 | 101, 104,
105 | 3eqtrd 2776 |
. . . . . . . . 9
β’ (((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β§ π₯ β (π΄ β (β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ)βπ₯) = (0gβπ»)) |
107 | 93, 106 | suppss 8175 |
. . . . . . . 8
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ) supp (0gβπ»)) β (β‘πΉ β (V β { 0 }))) |
108 | 107, 85 | sseqtrrd 4022 |
. . . . . . 7
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β ((πΎ β πΉ) supp (0gβπ»)) β ran π) |
109 | | eqid 2732 |
. . . . . . 7
β’ (((πΎ β πΉ) β π) supp (0gβπ»)) = (((πΎ β πΉ) β π) supp (0gβπ»)) |
110 | 27, 3, 67, 90, 91, 78, 93, 98, 63, 57, 108, 109 | gsumval3 19769 |
. . . . . 6
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (π» Ξ£g
(πΎ β πΉ)) =
(seq1((+gβπ»), ((πΎ β πΉ) β π))β(β―β(β‘πΉ β (V β { 0 }))))) |
111 | 76, 89, 110 | 3eqtr4rd 2783 |
. . . . 5
β’ ((π β§ ((β―β(β‘πΉ β (V β { 0 }))) β β β§
π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })))) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) |
112 | 111 | expr 457 |
. . . 4
β’ ((π β§ (β―β(β‘πΉ β (V β { 0 }))) β β)
β (π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
113 | 112 | exlimdv 1936 |
. . 3
β’ ((π β§ (β―β(β‘πΉ β (V β { 0 }))) β β)
β (βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 })) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
114 | 113 | expimpd 454 |
. 2
β’ (π β (((β―β(β‘πΉ β (V β { 0 }))) β β β§
βπ π:(1...(β―β(β‘πΉ β (V β { 0 }))))β1-1-ontoβ(β‘πΉ β (V β { 0 }))) β (π» Ξ£g
(πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ)))) |
115 | | gsumzmhm.w |
. . . . 5
β’ (π β πΉ finSupp 0 ) |
116 | 115 | fsuppimpd 9365 |
. . . 4
β’ (π β (πΉ supp 0 ) β
Fin) |
117 | 23, 116 | eqeltrrd 2834 |
. . 3
β’ (π β (β‘πΉ β (V β { 0 })) β
Fin) |
118 | | fz1f1o 15652 |
. . 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 858 |
1
β’ (π β (π» Ξ£g (πΎ β πΉ)) = (πΎβ(πΊ Ξ£g πΉ))) |