Step | Hyp | Ref
| Expression |
1 | | gsumval3.g |
. . . . 5
β’ (π β πΊ β Mnd) |
2 | | gsumval3.a |
. . . . 5
β’ (π β π΄ β π) |
3 | | gsumval3.0 |
. . . . . 6
β’ 0 =
(0gβπΊ) |
4 | 3 | gsumz 18651 |
. . . . 5
β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π₯ β π΄ β¦ 0 )) = 0 ) |
5 | 1, 2, 4 | syl2anc 585 |
. . . 4
β’ (π β (πΊ Ξ£g (π₯ β π΄ β¦ 0 )) = 0 ) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β§ π = β
) β (πΊ Ξ£g (π₯ β π΄ β¦ 0 )) = 0 ) |
7 | | gsumval3.f |
. . . . . . 7
β’ (π β πΉ:π΄βΆπ΅) |
8 | 7 | feqmptd 6911 |
. . . . . 6
β’ (π β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π = β
) β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
10 | | gsumval3.h |
. . . . . . . . . . . . . 14
β’ (π β π»:(1...π)β1-1βπ΄) |
11 | | f1f 6739 |
. . . . . . . . . . . . . 14
β’ (π»:(1...π)β1-1βπ΄ β π»:(1...π)βΆπ΄) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π»:(1...π)βΆπ΄) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π = β
) β§ π₯ β ran π») β π»:(1...π)βΆπ΄) |
14 | | f1f1orn 6796 |
. . . . . . . . . . . . . . . 16
β’ (π»:(1...π)β1-1βπ΄ β π»:(1...π)β1-1-ontoβran
π») |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π»:(1...π)β1-1-ontoβran
π») |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = β
) β π»:(1...π)β1-1-ontoβran
π») |
17 | | f1ocnv 6797 |
. . . . . . . . . . . . . 14
β’ (π»:(1...π)β1-1-ontoβran
π» β β‘π»:ran π»β1-1-ontoβ(1...π)) |
18 | | f1of 6785 |
. . . . . . . . . . . . . 14
β’ (β‘π»:ran π»β1-1-ontoβ(1...π) β β‘π»:ran π»βΆ(1...π)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((π β§ π = β
) β β‘π»:ran π»βΆ(1...π)) |
20 | 19 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ (((π β§ π = β
) β§ π₯ β ran π») β (β‘π»βπ₯) β (1...π)) |
21 | | fvco3 6941 |
. . . . . . . . . . . 12
β’ ((π»:(1...π)βΆπ΄ β§ (β‘π»βπ₯) β (1...π)) β ((πΉ β π»)β(β‘π»βπ₯)) = (πΉβ(π»β(β‘π»βπ₯)))) |
22 | 13, 20, 21 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π = β
) β§ π₯ β ran π») β ((πΉ β π»)β(β‘π»βπ₯)) = (πΉβ(π»β(β‘π»βπ₯)))) |
23 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = β
) β π = β
) |
24 | 23 | difeq2d 4083 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = β
) β ((1...π) β π) = ((1...π) β β
)) |
25 | | dif0 4333 |
. . . . . . . . . . . . . . 15
β’
((1...π) β
β
) = (1...π) |
26 | 24, 25 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = β
) β ((1...π) β π) = (1...π)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π = β
) β§ π₯ β ran π») β ((1...π) β π) = (1...π)) |
28 | 20, 27 | eleqtrrd 2837 |
. . . . . . . . . . . 12
β’ (((π β§ π = β
) β§ π₯ β ran π») β (β‘π»βπ₯) β ((1...π) β π)) |
29 | | fco 6693 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆπ΅ β§ π»:(1...π)βΆπ΄) β (πΉ β π»):(1...π)βΆπ΅) |
30 | 7, 12, 29 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ β π»):(1...π)βΆπ΅) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π = β
) β (πΉ β π»):(1...π)βΆπ΅) |
32 | | gsumval3.w |
. . . . . . . . . . . . . . 15
β’ π = ((πΉ β π») supp 0 ) |
33 | 32 | eqimss2i 4004 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π») supp 0 ) β π |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π = β
) β ((πΉ β π») supp 0 ) β π) |
35 | | ovexd 7393 |
. . . . . . . . . . . . 13
β’ ((π β§ π = β
) β (1...π) β V) |
36 | 3 | fvexi 6857 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π = β
) β 0 β V) |
38 | 31, 34, 35, 37 | suppssr 8128 |
. . . . . . . . . . . 12
β’ (((π β§ π = β
) β§ (β‘π»βπ₯) β ((1...π) β π)) β ((πΉ β π»)β(β‘π»βπ₯)) = 0 ) |
39 | 28, 38 | syldan 592 |
. . . . . . . . . . 11
β’ (((π β§ π = β
) β§ π₯ β ran π») β ((πΉ β π»)β(β‘π»βπ₯)) = 0 ) |
40 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . 13
β’ ((π»:(1...π)β1-1-ontoβran
π» β§ π₯ β ran π») β (π»β(β‘π»βπ₯)) = π₯) |
41 | 16, 40 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π = β
) β§ π₯ β ran π») β (π»β(β‘π»βπ₯)) = π₯) |
42 | 41 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π β§ π = β
) β§ π₯ β ran π») β (πΉβ(π»β(β‘π»βπ₯))) = (πΉβπ₯)) |
43 | 22, 39, 42 | 3eqtr3rd 2782 |
. . . . . . . . . 10
β’ (((π β§ π = β
) β§ π₯ β ran π») β (πΉβπ₯) = 0 ) |
44 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πΉβπ₯) β V |
45 | 44 | elsn 4602 |
. . . . . . . . . 10
β’ ((πΉβπ₯) β { 0 } β (πΉβπ₯) = 0 ) |
46 | 43, 45 | sylibr 233 |
. . . . . . . . 9
β’ (((π β§ π = β
) β§ π₯ β ran π») β (πΉβπ₯) β { 0 }) |
47 | 46 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ π = β
) β§ π₯ β π΄) β§ π₯ β ran π») β (πΉβπ₯) β { 0 }) |
48 | | eldif 3921 |
. . . . . . . . . . 11
β’ (π₯ β (π΄ β ran π») β (π₯ β π΄ β§ Β¬ π₯ β ran π»)) |
49 | | gsumval3.n |
. . . . . . . . . . . . 13
β’ (π β (πΉ supp 0 ) β ran π») |
50 | 36 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 0 β V) |
51 | 7, 49, 2, 50 | suppssr 8128 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β ran π»)) β (πΉβπ₯) = 0 ) |
52 | 51, 45 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄ β ran π»)) β (πΉβπ₯) β { 0 }) |
53 | 48, 52 | sylan2br 596 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β§ Β¬ π₯ β ran π»)) β (πΉβπ₯) β { 0 }) |
54 | 53 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π = β
) β§ (π₯ β π΄ β§ Β¬ π₯ β ran π»)) β (πΉβπ₯) β { 0 }) |
55 | 54 | anassrs 469 |
. . . . . . . 8
β’ ((((π β§ π = β
) β§ π₯ β π΄) β§ Β¬ π₯ β ran π») β (πΉβπ₯) β { 0 }) |
56 | 47, 55 | pm2.61dan 812 |
. . . . . . 7
β’ (((π β§ π = β
) β§ π₯ β π΄) β (πΉβπ₯) β { 0 }) |
57 | 56, 45 | sylib 217 |
. . . . . 6
β’ (((π β§ π = β
) β§ π₯ β π΄) β (πΉβπ₯) = 0 ) |
58 | 57 | mpteq2dva 5206 |
. . . . 5
β’ ((π β§ π = β
) β (π₯ β π΄ β¦ (πΉβπ₯)) = (π₯ β π΄ β¦ 0 )) |
59 | 9, 58 | eqtrd 2773 |
. . . 4
β’ ((π β§ π = β
) β πΉ = (π₯ β π΄ β¦ 0 )) |
60 | 59 | oveq2d 7374 |
. . 3
β’ ((π β§ π = β
) β (πΊ Ξ£g πΉ) = (πΊ Ξ£g (π₯ β π΄ β¦ 0 ))) |
61 | | gsumval3.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
62 | 61, 3 | mndidcl 18576 |
. . . . . 6
β’ (πΊ β Mnd β 0 β π΅) |
63 | | gsumval3.p |
. . . . . . 7
β’ + =
(+gβπΊ) |
64 | 61, 63, 3 | mndlid 18581 |
. . . . . 6
β’ ((πΊ β Mnd β§ 0 β π΅) β ( 0 + 0 ) = 0 ) |
65 | 1, 62, 64 | syl2anc2 586 |
. . . . 5
β’ (π β ( 0 + 0 ) = 0 ) |
66 | 65 | adantr 482 |
. . . 4
β’ ((π β§ π = β
) β ( 0 + 0 ) = 0 ) |
67 | | gsumval3.m |
. . . . . 6
β’ (π β π β β) |
68 | | nnuz 12811 |
. . . . . 6
β’ β =
(β€β₯β1) |
69 | 67, 68 | eleqtrdi 2844 |
. . . . 5
β’ (π β π β
(β€β₯β1)) |
70 | 69 | adantr 482 |
. . . 4
β’ ((π β§ π = β
) β π β
(β€β₯β1)) |
71 | 26 | eleq2d 2820 |
. . . . . 6
β’ ((π β§ π = β
) β (π₯ β ((1...π) β π) β π₯ β (1...π))) |
72 | 71 | biimpar 479 |
. . . . 5
β’ (((π β§ π = β
) β§ π₯ β (1...π)) β π₯ β ((1...π) β π)) |
73 | 31, 34, 35, 37 | suppssr 8128 |
. . . . 5
β’ (((π β§ π = β
) β§ π₯ β ((1...π) β π)) β ((πΉ β π»)βπ₯) = 0 ) |
74 | 72, 73 | syldan 592 |
. . . 4
β’ (((π β§ π = β
) β§ π₯ β (1...π)) β ((πΉ β π»)βπ₯) = 0 ) |
75 | 66, 70, 74 | seqid3 13958 |
. . 3
β’ ((π β§ π = β
) β (seq1( + , (πΉ β π»))βπ) = 0 ) |
76 | 6, 60, 75 | 3eqtr4d 2783 |
. 2
β’ ((π β§ π = β
) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ)) |
77 | | fzf 13434 |
. . . . 5
β’
...:(β€ Γ β€)βΆπ« β€ |
78 | | ffn 6669 |
. . . . 5
β’
(...:(β€ Γ β€)βΆπ« β€ β ... Fn
(β€ Γ β€)) |
79 | | ovelrn 7531 |
. . . . 5
β’ (... Fn
(β€ Γ β€) β (π΄ β ran ... β βπ β β€ βπ β β€ π΄ = (π...π))) |
80 | 77, 78, 79 | mp2b 10 |
. . . 4
β’ (π΄ β ran ... β
βπ β β€
βπ β β€
π΄ = (π...π)) |
81 | 1 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β πΊ β Mnd) |
82 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β π΄ = (π...π)) |
83 | | frel 6674 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:π΄βΆπ΅ β Rel πΉ) |
84 | | reldm0 5884 |
. . . . . . . . . . . . . . . . 17
β’ (Rel
πΉ β (πΉ = β
β dom πΉ = β
)) |
85 | 7, 83, 84 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ = β
β dom πΉ = β
)) |
86 | 7 | fdmd 6680 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom πΉ = π΄) |
87 | 86 | eqeq1d 2735 |
. . . . . . . . . . . . . . . 16
β’ (π β (dom πΉ = β
β π΄ = β
)) |
88 | 85, 87 | bitrd 279 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ = β
β π΄ = β
)) |
89 | | coeq1 5814 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ = β
β (πΉ β π») = (β
β π»)) |
90 | | co01 6214 |
. . . . . . . . . . . . . . . . . . 19
β’ (β
β π») =
β
|
91 | 89, 90 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ = β
β (πΉ β π») = β
) |
92 | 91 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ = β
β ((πΉ β π») supp 0 ) = (β
supp 0
)) |
93 | | supp0 8098 |
. . . . . . . . . . . . . . . . . 18
β’ ( 0 β V
β (β
supp 0 ) =
β
) |
94 | 36, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (β
supp 0 )
= β
|
95 | 92, 94 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
β’ (πΉ = β
β ((πΉ β π») supp 0 ) =
β
) |
96 | 32, 95 | eqtrid 2785 |
. . . . . . . . . . . . . . 15
β’ (πΉ = β
β π = β
) |
97 | 88, 96 | syl6bir 254 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ = β
β π = β
)) |
98 | 97 | necon3d 2961 |
. . . . . . . . . . . . 13
β’ (π β (π β β
β π΄ β β
)) |
99 | 98 | imp 408 |
. . . . . . . . . . . 12
β’ ((π β§ π β β
) β π΄ β β
) |
100 | 99 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β π΄ β β
) |
101 | 82, 100 | eqnetrrd 3009 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (π...π) β β
) |
102 | | fzn0 13461 |
. . . . . . . . . 10
β’ ((π...π) β β
β π β (β€β₯βπ)) |
103 | 101, 102 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β π β (β€β₯βπ)) |
104 | 7 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β πΉ:π΄βΆπ΅) |
105 | 82 | feq2d 6655 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (πΉ:π΄βΆπ΅ β πΉ:(π...π)βΆπ΅)) |
106 | 104, 105 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β πΉ:(π...π)βΆπ΅) |
107 | 61, 63, 81, 103, 106 | gsumval2 18546 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (πΊ Ξ£g πΉ) = (seqπ( + , πΉ)βπ)) |
108 | | frn 6676 |
. . . . . . . . . . . . . . 15
β’ (π»:(1...π)βΆπ΄ β ran π» β π΄) |
109 | 10, 11, 108 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β ran π» β π΄) |
110 | 109 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β ran π» β π΄) |
111 | 110, 82 | sseqtrd 3985 |
. . . . . . . . . . . 12
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β ran π» β (π...π)) |
112 | | fzssuz 13488 |
. . . . . . . . . . . . 13
β’ (π...π) β (β€β₯βπ) |
113 | | uzssz 12789 |
. . . . . . . . . . . . . 14
β’
(β€β₯βπ) β β€ |
114 | | zssre 12511 |
. . . . . . . . . . . . . 14
β’ β€
β β |
115 | 113, 114 | sstri 3954 |
. . . . . . . . . . . . 13
β’
(β€β₯βπ) β β |
116 | 112, 115 | sstri 3954 |
. . . . . . . . . . . 12
β’ (π...π) β β |
117 | 111, 116 | sstrdi 3957 |
. . . . . . . . . . 11
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β ran π» β β) |
118 | | ltso 11240 |
. . . . . . . . . . 11
β’ < Or
β |
119 | | soss 5566 |
. . . . . . . . . . 11
β’ (ran
π» β β β (
< Or β β < Or ran π»)) |
120 | 117, 118,
119 | mpisyl 21 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β < Or ran π») |
121 | | fzfi 13883 |
. . . . . . . . . . . 12
β’
(1...π) β
Fin |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β Fin) |
123 | 12, 122 | fexd 7178 |
. . . . . . . . . . . . . 14
β’ (π β π» β V) |
124 | | f1oen3g 8909 |
. . . . . . . . . . . . . 14
β’ ((π» β V β§ π»:(1...π)β1-1-ontoβran
π») β (1...π) β ran π») |
125 | 123, 15, 124 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β ran π») |
126 | | enfi 9137 |
. . . . . . . . . . . . 13
β’
((1...π) β ran
π» β ((1...π) β Fin β ran π» β Fin)) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((1...π) β Fin β ran π» β Fin)) |
128 | 121, 127 | mpbii 232 |
. . . . . . . . . . 11
β’ (π β ran π» β Fin) |
129 | 128 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β ran π» β Fin) |
130 | | fz1iso 14367 |
. . . . . . . . . 10
β’ (( <
Or ran π» β§ ran π» β Fin) β βπ π Isom < , < ((1...(β―βran
π»)), ran π»)) |
131 | 120, 129,
130 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β βπ π Isom < , < ((1...(β―βran
π»)), ran π»)) |
132 | 67 | nnnn0d 12478 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
133 | | hashfz1 14252 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (β―β(1...π)) = π) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β(1...π)) = π) |
135 | 122, 15 | hasheqf1od 14259 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β(1...π)) = (β―βran π»)) |
136 | 134, 135 | eqtr3d 2775 |
. . . . . . . . . . . . . 14
β’ (π β π = (β―βran π»)) |
137 | 136 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π = (β―βran π»)) |
138 | 137 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (seq1( + , (πΉ β π))βπ) = (seq1( + , (πΉ β π))β(β―βran π»))) |
139 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β πΊ β Mnd) |
140 | 61, 63 | mndcl 18569 |
. . . . . . . . . . . . . . 15
β’ ((πΊ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) |
141 | 140 | 3expb 1121 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
142 | 139, 141 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
143 | | gsumval3.c |
. . . . . . . . . . . . . . . . 17
β’ (π β ran πΉ β (πβran πΉ)) |
144 | 143 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ran πΉ β (πβran πΉ)) |
145 | 144 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β ran πΉ) β π₯ β (πβran πΉ)) |
146 | | gsumval3.z |
. . . . . . . . . . . . . . . 16
β’ π = (CntzβπΊ) |
147 | 63, 146 | cntzi 19114 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (πβran πΉ) β§ π¦ β ran πΉ) β (π₯ + π¦) = (π¦ + π₯)) |
148 | 145, 147 | sylan 581 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β ran πΉ) β§ π¦ β ran πΉ) β (π₯ + π¦) = (π¦ + π₯)) |
149 | 148 | anasss 468 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ (π₯ β ran πΉ β§ π¦ β ran πΉ)) β (π₯ + π¦) = (π¦ + π₯)) |
150 | 61, 63 | mndass 18570 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
151 | 139, 150 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
152 | 69 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π β
(β€β₯β1)) |
153 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β πΉ:π΄βΆπ΅) |
154 | 153 | frnd 6677 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ran πΉ β π΅) |
155 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π Isom < , < ((1...(β―βran
π»)), ran π»)) |
156 | | isof1o 7269 |
. . . . . . . . . . . . . . . . 17
β’ (π Isom < , <
((1...(β―βran π»)), ran π») β π:(1...(β―βran π»))β1-1-ontoβran
π») |
157 | 155, 156 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π:(1...(β―βran π»))β1-1-ontoβran
π») |
158 | 137 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (1...π) = (1...(β―βran π»))) |
159 | 158 | f1oeq2d 6781 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (π:(1...π)β1-1-ontoβran
π» β π:(1...(β―βran π»))β1-1-ontoβran
π»)) |
160 | 157, 159 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π:(1...π)β1-1-ontoβran
π») |
161 | | f1ocnv 6797 |
. . . . . . . . . . . . . . 15
β’ (π:(1...π)β1-1-ontoβran
π» β β‘π:ran π»β1-1-ontoβ(1...π)) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β β‘π:ran π»β1-1-ontoβ(1...π)) |
163 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π»:(1...π)β1-1-ontoβran
π») |
164 | | f1oco 6808 |
. . . . . . . . . . . . . 14
β’ ((β‘π:ran π»β1-1-ontoβ(1...π) β§ π»:(1...π)β1-1-ontoβran
π») β (β‘π β π»):(1...π)β1-1-ontoβ(1...π)) |
165 | 162, 163,
164 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (β‘π β π»):(1...π)β1-1-ontoβ(1...π)) |
166 | | ffn 6669 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
167 | | dffn4 6763 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ Fn π΄ β πΉ:π΄βontoβran πΉ) |
168 | 166, 167 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βontoβran πΉ) |
169 | | fof 6757 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:π΄βontoβran πΉ β πΉ:π΄βΆran πΉ) |
170 | 153, 168,
169 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β πΉ:π΄βΆran πΉ) |
171 | | f1of 6785 |
. . . . . . . . . . . . . . . . 17
β’ (π:(1...π)β1-1-ontoβran
π» β π:(1...π)βΆran π») |
172 | 160, 171 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π:(1...π)βΆran π») |
173 | 109 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ran π» β π΄) |
174 | 172, 173 | fssd 6687 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π:(1...π)βΆπ΄) |
175 | | fco 6693 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π΄βΆran πΉ β§ π:(1...π)βΆπ΄) β (πΉ β π):(1...π)βΆran πΉ) |
176 | 170, 174,
175 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (πΉ β π):(1...π)βΆran πΉ) |
177 | 176 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β (1...π)) β ((πΉ β π)βπ₯) β ran πΉ) |
178 | | f1ococnv2 6812 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:(1...π)β1-1-ontoβran
π» β (π β β‘π) = ( I βΎ ran π»)) |
179 | 160, 178 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (π β β‘π) = ( I βΎ ran π»)) |
180 | 179 | coeq1d 5818 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ((π β β‘π) β π») = (( I βΎ ran π») β π»)) |
181 | | f1of 6785 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π»:(1...π)β1-1-ontoβran
π» β π»:(1...π)βΆran π») |
182 | | fcoi2 6718 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π»:(1...π)βΆran π» β (( I βΎ ran π») β π») = π») |
183 | 163, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (( I βΎ ran π») β π») = π») |
184 | 180, 183 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π» = ((π β β‘π) β π»)) |
185 | | coass 6218 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β‘π) β π») = (π β (β‘π β π»)) |
186 | 184, 185 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π» = (π β (β‘π β π»))) |
187 | 186 | coeq2d 5819 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (πΉ β π») = (πΉ β (π β (β‘π β π»)))) |
188 | | coass 6218 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β π) β (β‘π β π»)) = (πΉ β (π β (β‘π β π»))) |
189 | 187, 188 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (πΉ β π») = ((πΉ β π) β (β‘π β π»))) |
190 | 189 | fveq1d 6845 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ((πΉ β π»)βπ) = (((πΉ β π) β (β‘π β π»))βπ)) |
191 | 190 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π β (1...π)) β ((πΉ β π»)βπ) = (((πΉ β π) β (β‘π β π»))βπ)) |
192 | | f1of 6785 |
. . . . . . . . . . . . . . . . 17
β’ (β‘π:ran π»β1-1-ontoβ(1...π) β β‘π:ran π»βΆ(1...π)) |
193 | 160, 161,
192 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β β‘π:ran π»βΆ(1...π)) |
194 | 163, 181 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π»:(1...π)βΆran π») |
195 | | fco 6693 |
. . . . . . . . . . . . . . . 16
β’ ((β‘π:ran π»βΆ(1...π) β§ π»:(1...π)βΆran π») β (β‘π β π»):(1...π)βΆ(1...π)) |
196 | 193, 194,
195 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (β‘π β π»):(1...π)βΆ(1...π)) |
197 | | fvco3 6941 |
. . . . . . . . . . . . . . 15
β’ (((β‘π β π»):(1...π)βΆ(1...π) β§ π β (1...π)) β (((πΉ β π) β (β‘π β π»))βπ) = ((πΉ β π)β((β‘π β π»)βπ))) |
198 | 196, 197 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π β (1...π)) β (((πΉ β π) β (β‘π β π»))βπ) = ((πΉ β π)β((β‘π β π»)βπ))) |
199 | 191, 198 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π β (1...π)) β ((πΉ β π»)βπ) = ((πΉ β π)β((β‘π β π»)βπ))) |
200 | 142, 149,
151, 152, 154, 165, 177, 199 | seqf1o 13955 |
. . . . . . . . . . . 12
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (seq1( + , (πΉ β π»))βπ) = (seq1( + , (πΉ β π))βπ)) |
201 | 61, 63, 3 | mndlid 18581 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Mnd β§ π₯ β π΅) β ( 0 + π₯) = π₯) |
202 | 139, 201 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β π΅) β ( 0 + π₯) = π₯) |
203 | 61, 63, 3 | mndrid 18582 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Mnd β§ π₯ β π΅) β (π₯ + 0 ) = π₯) |
204 | 139, 203 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β π΅) β (π₯ + 0 ) = π₯) |
205 | 139, 62 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β 0 β π΅) |
206 | | fdm 6678 |
. . . . . . . . . . . . . . . . 17
β’ (π»:(1...π)βΆπ΄ β dom π» = (1...π)) |
207 | 10, 11, 206 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β dom π» = (1...π)) |
208 | | eluzfz1 13454 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β1) β 1 β (1...π)) |
209 | | ne0i 4295 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
(1...π) β (1...π) β β
) |
210 | 69, 208, 209 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β β
) |
211 | 207, 210 | eqnetrd 3008 |
. . . . . . . . . . . . . . 15
β’ (π β dom π» β β
) |
212 | | dm0rn0 5881 |
. . . . . . . . . . . . . . . 16
β’ (dom
π» = β
β ran
π» =
β
) |
213 | 212 | necon3bii 2993 |
. . . . . . . . . . . . . . 15
β’ (dom
π» β β
β ran
π» β
β
) |
214 | 211, 213 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β ran π» β β
) |
215 | 214 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ran π» β β
) |
216 | 111 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β ran π» β (π...π)) |
217 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π΄ = (π...π)) |
218 | 217 | eleq2d 2820 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (π₯ β π΄ β π₯ β (π...π))) |
219 | 218 | biimpar 479 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β (π...π)) β π₯ β π΄) |
220 | 153 | ffvelcdmda 7036 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β π΄) β (πΉβπ₯) β π΅) |
221 | 219, 220 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β (π...π)) β (πΉβπ₯) β π΅) |
222 | 217 | difeq1d 4082 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (π΄ β ran π») = ((π...π) β ran π»)) |
223 | 222 | eleq2d 2820 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (π₯ β (π΄ β ran π») β π₯ β ((π...π) β ran π»))) |
224 | 223 | biimpar 479 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β ((π...π) β ran π»)) β π₯ β (π΄ β ran π»)) |
225 | 51 | ad4ant14 751 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β (π΄ β ran π»)) β (πΉβπ₯) = 0 ) |
226 | 224, 225 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π₯ β ((π...π) β ran π»)) β (πΉβπ₯) = 0 ) |
227 | | f1of 6785 |
. . . . . . . . . . . . . . 15
β’ (π:(1...(β―βran π»))β1-1-ontoβran
π» β π:(1...(β―βran π»))βΆran π») |
228 | 155, 156,
227 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β π:(1...(β―βran π»))βΆran π») |
229 | | fvco3 6941 |
. . . . . . . . . . . . . 14
β’ ((π:(1...(β―βran π»))βΆran π» β§ π¦ β (1...(β―βran π»))) β ((πΉ β π)βπ¦) = (πΉβ(πβπ¦))) |
230 | 228, 229 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β§ π¦ β (1...(β―βran π»))) β ((πΉ β π)βπ¦) = (πΉβ(πβπ¦))) |
231 | 202, 204,
142, 205, 155, 215, 216, 221, 226, 230 | seqcoll2 14370 |
. . . . . . . . . . . 12
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (seqπ( + , πΉ)βπ) = (seq1( + , (πΉ β π))β(β―βran π»))) |
232 | 138, 200,
231 | 3eqtr4d 2783 |
. . . . . . . . . . 11
β’ (((π β§ π β β
) β§ (π΄ = (π...π) β§ π Isom < , < ((1...(β―βran
π»)), ran π»))) β (seq1( + , (πΉ β π»))βπ) = (seqπ( + , πΉ)βπ)) |
233 | 232 | expr 458 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (π Isom < , < ((1...(β―βran
π»)), ran π») β (seq1( + , (πΉ β π»))βπ) = (seqπ( + , πΉ)βπ))) |
234 | 233 | exlimdv 1937 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (βπ π Isom < , < ((1...(β―βran
π»)), ran π») β (seq1( + , (πΉ β π»))βπ) = (seqπ( + , πΉ)βπ))) |
235 | 131, 234 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (seq1( + , (πΉ β π»))βπ) = (seqπ( + , πΉ)βπ)) |
236 | 107, 235 | eqtr4d 2776 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π΄ = (π...π)) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ)) |
237 | 236 | ex 414 |
. . . . . 6
β’ ((π β§ π β β
) β (π΄ = (π...π) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ))) |
238 | 237 | rexlimdvw 3154 |
. . . . 5
β’ ((π β§ π β β
) β (βπ β β€ π΄ = (π...π) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ))) |
239 | 238 | rexlimdvw 3154 |
. . . 4
β’ ((π β§ π β β
) β (βπ β β€ βπ β β€ π΄ = (π...π) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ))) |
240 | 80, 239 | biimtrid 241 |
. . 3
β’ ((π β§ π β β
) β (π΄ β ran ... β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ))) |
241 | | suppssdm 8109 |
. . . . . . . . . . 11
β’ ((πΉ β π») supp 0 ) β dom (πΉ β π») |
242 | 32, 241 | eqsstri 3979 |
. . . . . . . . . 10
β’ π β dom (πΉ β π») |
243 | 242, 30 | fssdm 6689 |
. . . . . . . . 9
β’ (π β π β (1...π)) |
244 | | fz1ssnn 13478 |
. . . . . . . . . 10
β’
(1...π) β
β |
245 | | nnssre 12162 |
. . . . . . . . . 10
β’ β
β β |
246 | 244, 245 | sstri 3954 |
. . . . . . . . 9
β’
(1...π) β
β |
247 | 243, 246 | sstrdi 3957 |
. . . . . . . 8
β’ (π β π β β) |
248 | | soss 5566 |
. . . . . . . 8
β’ (π β β β ( <
Or β β < Or π)) |
249 | 247, 118,
248 | mpisyl 21 |
. . . . . . 7
β’ (π β < Or π) |
250 | | ssfi 9120 |
. . . . . . . 8
β’
(((1...π) β Fin
β§ π β (1...π)) β π β Fin) |
251 | 121, 243,
250 | sylancr 588 |
. . . . . . 7
β’ (π β π β Fin) |
252 | | fz1iso 14367 |
. . . . . . 7
β’ (( <
Or π β§ π β Fin) β βπ π Isom < , < ((1...(β―βπ)), π)) |
253 | 249, 251,
252 | syl2anc 585 |
. . . . . 6
β’ (π β βπ π Isom < , < ((1...(β―βπ)), π)) |
254 | 253 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β
) β§ Β¬ π΄ β ran ...) β βπ π Isom < , < ((1...(β―βπ)), π)) |
255 | 61, 3, 63, 146, 1, 2, 7, 143, 67, 10, 49, 32 | gsumval3lem2 19688 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ))) |
256 | 1 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β πΊ β Mnd) |
257 | 256, 201 | sylan 581 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ π₯ β π΅) β ( 0 + π₯) = π₯) |
258 | 256, 203 | sylan 581 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ π₯ β π΅) β (π₯ + 0 ) = π₯) |
259 | 256, 141 | sylan 581 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
260 | 256, 62 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β 0 β π΅) |
261 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π Isom < , <
((1...(β―βπ)),
π)) |
262 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π β β
) |
263 | 243 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π β (1...π)) |
264 | 30 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΉ β π»):(1...π)βΆπ΅) |
265 | 264 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ π₯ β (1...π)) β ((πΉ β π»)βπ₯) β π΅) |
266 | 33 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((πΉ β π») supp 0 ) β π) |
267 | | ovexd 7393 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (1...π) β V) |
268 | 36 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β 0 β
V) |
269 | 264, 266,
267, 268 | suppssr 8128 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ π₯ β ((1...π) β π)) β ((πΉ β π»)βπ₯) = 0 ) |
270 | | coass 6218 |
. . . . . . . . . . 11
β’ ((πΉ β π») β π) = (πΉ β (π» β π)) |
271 | 270 | fveq1i 6844 |
. . . . . . . . . 10
β’ (((πΉ β π») β π)βπ¦) = ((πΉ β (π» β π))βπ¦) |
272 | | isof1o 7269 |
. . . . . . . . . . . 12
β’ (π Isom < , <
((1...(β―βπ)),
π) β π:(1...(β―βπ))β1-1-ontoβπ) |
273 | | f1of 6785 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπ))β1-1-ontoβπ β π:(1...(β―βπ))βΆπ) |
274 | 261, 272,
273 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π:(1...(β―βπ))βΆπ) |
275 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ))βΆπ β§ π¦ β (1...(β―βπ))) β (((πΉ β π») β π)βπ¦) = ((πΉ β π»)β(πβπ¦))) |
276 | 274, 275 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ π¦ β
(1...(β―βπ)))
β (((πΉ β π») β π)βπ¦) = ((πΉ β π»)β(πβπ¦))) |
277 | 271, 276 | eqtr3id 2787 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β§ π¦ β
(1...(β―βπ)))
β ((πΉ β (π» β π))βπ¦) = ((πΉ β π»)β(πβπ¦))) |
278 | 257, 258,
259, 260, 261, 262, 263, 265, 269, 277 | seqcoll2 14370 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (seq1( + , (πΉ β π»))βπ) = (seq1( + , (πΉ β (π» β π)))β(β―βπ))) |
279 | 255, 278 | eqtr4d 2776 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β π»))βπ)) |
280 | 279 | expr 458 |
. . . . . 6
β’ (((π β§ π β β
) β§ Β¬ π΄ β ran ...) β (π Isom < , < ((1...(β―βπ)), π) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ))) |
281 | 280 | exlimdv 1937 |
. . . . 5
β’ (((π β§ π β β
) β§ Β¬ π΄ β ran ...) β (βπ π Isom < , < ((1...(β―βπ)), π) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ))) |
282 | 254, 281 | mpd 15 |
. . . 4
β’ (((π β§ π β β
) β§ Β¬ π΄ β ran ...) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ)) |
283 | 282 | ex 414 |
. . 3
β’ ((π β§ π β β
) β (Β¬ π΄ β ran ... β (πΊ Ξ£g
πΉ) = (seq1( + , (πΉ β π»))βπ))) |
284 | 240, 283 | pm2.61d 179 |
. 2
β’ ((π β§ π β β
) β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ)) |
285 | 76, 284 | pm2.61dane 3029 |
1
β’ (π β (πΊ Ξ£g πΉ) = (seq1( + , (πΉ β π»))βπ)) |