Step | Hyp | Ref
| Expression |
1 | | gsumval3.h |
. . . . . . 7
β’ (π β π»:(1...π)β1-1βπ΄) |
2 | 1 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π»:(1...π)β1-1βπ΄) |
3 | | gsumval3.w |
. . . . . . . . 9
β’ π = ((πΉ β π») supp 0 ) |
4 | | suppssdm 8113 |
. . . . . . . . 9
β’ ((πΉ β π») supp 0 ) β dom (πΉ β π») |
5 | 3, 4 | eqsstri 3983 |
. . . . . . . 8
β’ π β dom (πΉ β π») |
6 | | gsumval3.f |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆπ΅) |
7 | | f1f 6743 |
. . . . . . . . . 10
β’ (π»:(1...π)β1-1βπ΄ β π»:(1...π)βΆπ΄) |
8 | 1, 7 | syl 17 |
. . . . . . . . 9
β’ (π β π»:(1...π)βΆπ΄) |
9 | | fco 6697 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ π»:(1...π)βΆπ΄) β (πΉ β π»):(1...π)βΆπ΅) |
10 | 6, 8, 9 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΉ β π»):(1...π)βΆπ΅) |
11 | 5, 10 | fssdm 6693 |
. . . . . . 7
β’ (π β π β (1...π)) |
12 | 11 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π β (1...π)) |
13 | | f1ores 6803 |
. . . . . 6
β’ ((π»:(1...π)β1-1βπ΄ β§ π β (1...π)) β (π» βΎ π):πβ1-1-ontoβ(π» β π)) |
14 | 2, 12, 13 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» βΎ π):πβ1-1-ontoβ(π» β π)) |
15 | 3 | imaeq2i 6016 |
. . . . . . 7
β’ (π» β π) = (π» β ((πΉ β π») supp 0 )) |
16 | | gsumval3.a |
. . . . . . . . . . 11
β’ (π β π΄ β π) |
17 | 6, 16 | fexd 7182 |
. . . . . . . . . 10
β’ (π β πΉ β V) |
18 | | ovex 7395 |
. . . . . . . . . . . 12
β’
(1...π) β
V |
19 | | fex 7181 |
. . . . . . . . . . . 12
β’ ((π»:(1...π)βΆπ΄ β§ (1...π) β V) β π» β V) |
20 | 7, 18, 19 | sylancl 587 |
. . . . . . . . . . 11
β’ (π»:(1...π)β1-1βπ΄ β π» β V) |
21 | 1, 20 | syl 17 |
. . . . . . . . . 10
β’ (π β π» β V) |
22 | | f1fun 6745 |
. . . . . . . . . . . 12
β’ (π»:(1...π)β1-1βπ΄ β Fun π») |
23 | 1, 22 | syl 17 |
. . . . . . . . . . 11
β’ (π β Fun π») |
24 | | gsumval3.n |
. . . . . . . . . . 11
β’ (π β (πΉ supp 0 ) β ran π») |
25 | 23, 24 | jca 513 |
. . . . . . . . . 10
β’ (π β (Fun π» β§ (πΉ supp 0 ) β ran π»)) |
26 | 17, 21, 25 | jca31 516 |
. . . . . . . . 9
β’ (π β ((πΉ β V β§ π» β V) β§ (Fun π» β§ (πΉ supp 0 ) β ran π»))) |
27 | 26 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((πΉ β V β§ π» β V) β§ (Fun π» β§ (πΉ supp 0 ) β ran π»))) |
28 | | imacosupp 8145 |
. . . . . . . . 9
β’ ((πΉ β V β§ π» β V) β ((Fun π» β§ (πΉ supp 0 ) β ran π») β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 ))) |
29 | 28 | imp 408 |
. . . . . . . 8
β’ (((πΉ β V β§ π» β V) β§ (Fun π» β§ (πΉ supp 0 ) β ran π»)) β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 )) |
30 | 27, 29 | syl 17 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 )) |
31 | 15, 30 | eqtrid 2789 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π) = (πΉ supp 0 )) |
32 | 31 | f1oeq3d 6786 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((π» βΎ π):πβ1-1-ontoβ(π» β π) β (π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 ))) |
33 | 14, 32 | mpbid 231 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 )) |
34 | | isof1o 7273 |
. . . . 5
β’ (π Isom < , <
((1...(β―βπ)),
π) β π:(1...(β―βπ))β1-1-ontoβπ) |
35 | 34 | ad2antll 728 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π:(1...(β―βπ))β1-1-ontoβπ) |
36 | | f1oco 6812 |
. . . 4
β’ (((π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 ) β§ π:(1...(β―βπ))β1-1-ontoβπ) β ((π» βΎ π) β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 )) |
37 | 33, 35, 36 | syl2anc 585 |
. . 3
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((π» βΎ π) β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 )) |
38 | | f1of 6789 |
. . . . 5
β’ (π:(1...(β―βπ))β1-1-ontoβπ β π:(1...(β―βπ))βΆπ) |
39 | | frn 6680 |
. . . . 5
β’ (π:(1...(β―βπ))βΆπ β ran π β π) |
40 | 35, 38, 39 | 3syl 18 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ran π β π) |
41 | | cores 6206 |
. . . 4
β’ (ran
π β π β ((π» βΎ π) β π) = (π» β π)) |
42 | | f1oeq1 6777 |
. . . 4
β’ (((π» βΎ π) β π) = (π» β π) β (((π» βΎ π) β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 ) β (π» β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 ))) |
43 | 40, 41, 42 | 3syl 18 |
. . 3
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (((π» βΎ π) β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 ) β (π» β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 ))) |
44 | 37, 43 | mpbid 231 |
. 2
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 )) |
45 | | fzfi 13884 |
. . . . . . 7
β’
(1...π) β
Fin |
46 | | ssfi 9124 |
. . . . . . 7
β’
(((1...π) β Fin
β§ π β (1...π)) β π β Fin) |
47 | 45, 11, 46 | sylancr 588 |
. . . . . 6
β’ (π β π β Fin) |
48 | 47 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π β Fin) |
49 | 3 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β π = ((πΉ β π») supp 0 )) |
50 | 49 | imaeq2d 6018 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π) = (π» β ((πΉ β π») supp 0 ))) |
51 | 45 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1...π) β Fin) |
52 | 8, 51 | fexd 7182 |
. . . . . . . . . . 11
β’ (π β π» β V) |
53 | 17, 52, 25 | jca31 516 |
. . . . . . . . . 10
β’ (π β ((πΉ β V β§ π» β V) β§ (Fun π» β§ (πΉ supp 0 ) β ran π»))) |
54 | 53 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((πΉ β V β§ π» β V) β§ (Fun π» β§ (πΉ supp 0 ) β ran π»))) |
55 | 54, 29 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β ((πΉ β π») supp 0 )) = (πΉ supp 0 )) |
56 | 50, 55 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π) = (πΉ supp 0 )) |
57 | 56 | f1oeq3d 6786 |
. . . . . 6
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((π» βΎ π):πβ1-1-ontoβ(π» β π) β (π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 ))) |
58 | 14, 57 | mpbid 231 |
. . . . 5
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» βΎ π):πβ1-1-ontoβ(πΉ supp 0 )) |
59 | 48, 58 | hasheqf1od 14260 |
. . . 4
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β
(β―βπ) =
(β―β(πΉ supp
0
))) |
60 | 59 | oveq2d 7378 |
. . 3
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β
(1...(β―βπ)) =
(1...(β―β(πΉ supp
0
)))) |
61 | 60 | f1oeq2d 6785 |
. 2
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β ((π» β π):(1...(β―βπ))β1-1-ontoβ(πΉ supp 0 ) β (π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 ))) |
62 | 44, 61 | mpbid 231 |
1
β’ (((π β§ π β β
) β§ (Β¬ π΄ β ran ... β§ π Isom < , <
((1...(β―βπ)),
π))) β (π» β π):(1...(β―β(πΉ supp 0 )))β1-1-ontoβ(πΉ supp 0 )) |