Step | Hyp | Ref
| Expression |
1 | | iscyg.1 |
. . 3
β’ π΅ = (BaseβπΊ) |
2 | | iscyg.2 |
. . 3
β’ Β· =
(.gβπΊ) |
3 | | iscyg3.e |
. . 3
β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} |
4 | 1, 2, 3 | iscyggen 19849 |
. 2
β’ (π β πΈ β (π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅)) |
5 | | simplr 767 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β π΅ β Fin) |
6 | | simplll 773 |
. . . . . . . . 9
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β πΊ β Grp) |
7 | | simpr 483 |
. . . . . . . . 9
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β π β β€) |
8 | | simplr 767 |
. . . . . . . . 9
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β π β π΅) |
9 | 1, 2 | mulgcl 19060 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π β β€ β§ π β π΅) β (π Β· π) β π΅) |
10 | 6, 7, 8, 9 | syl3anc 1368 |
. . . . . . . 8
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β (π Β· π) β π΅) |
11 | 10 | fmpttd 7130 |
. . . . . . 7
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (π β β€ β¦ (π Β· π)):β€βΆπ΅) |
12 | 11 | frnd 6735 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ran (π β β€ β¦ (π Β· π)) β π΅) |
13 | 5, 12 | ssfid 9300 |
. . . . 5
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ran (π β β€ β¦ (π Β· π)) β Fin) |
14 | | hashen 14348 |
. . . . 5
β’ ((ran
(π β β€ β¦
(π Β· π)) β Fin β§ π΅ β Fin) β ((β―βran
(π β β€ β¦
(π Β· π))) = (β―βπ΅) β ran (π β β€ β¦ (π Β· π)) β π΅)) |
15 | 13, 5, 14 | syl2anc 582 |
. . . 4
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ((β―βran (π β β€ β¦ (π Β· π))) = (β―βπ΅) β ran (π β β€ β¦ (π Β· π)) β π΅)) |
16 | | cyggenod.o |
. . . . . . . 8
β’ π = (odβπΊ) |
17 | | eqid 2728 |
. . . . . . . 8
β’ (π β β€ β¦ (π Β· π)) = (π β β€ β¦ (π Β· π)) |
18 | 1, 16, 2, 17 | dfod2 19533 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β π΅) β (πβπ) = if(ran (π β β€ β¦ (π Β· π)) β Fin, (β―βran (π β β€ β¦ (π Β· π))), 0)) |
19 | 18 | adantlr 713 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (πβπ) = if(ran (π β β€ β¦ (π Β· π)) β Fin, (β―βran (π β β€ β¦ (π Β· π))), 0)) |
20 | 13 | iftrued 4540 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β if(ran (π β β€ β¦ (π Β· π)) β Fin, (β―βran (π β β€ β¦ (π Β· π))), 0) = (β―βran (π β β€ β¦ (π Β· π)))) |
21 | 19, 20 | eqtr2d 2769 |
. . . . 5
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (β―βran (π β β€ β¦ (π Β· π))) = (πβπ)) |
22 | 21 | eqeq1d 2730 |
. . . 4
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ((β―βran (π β β€ β¦ (π Β· π))) = (β―βπ΅) β (πβπ) = (β―βπ΅))) |
23 | | fisseneq 9290 |
. . . . . . 7
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅ β§ ran (π β β€ β¦ (π Β· π)) β π΅) β ran (π β β€ β¦ (π Β· π)) = π΅) |
24 | 23 | 3expia 1118 |
. . . . . 6
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅) β (ran (π β β€ β¦ (π Β· π)) β π΅ β ran (π β β€ β¦ (π Β· π)) = π΅)) |
25 | | enrefg 9013 |
. . . . . . . 8
β’ (π΅ β Fin β π΅ β π΅) |
26 | 25 | adantr 479 |
. . . . . . 7
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅) β π΅ β π΅) |
27 | | breq1 5155 |
. . . . . . 7
β’ (ran
(π β β€ β¦
(π Β· π)) = π΅ β (ran (π β β€ β¦ (π Β· π)) β π΅ β π΅ β π΅)) |
28 | 26, 27 | syl5ibrcom 246 |
. . . . . 6
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅) β (ran (π β β€ β¦ (π Β· π)) = π΅ β ran (π β β€ β¦ (π Β· π)) β π΅)) |
29 | 24, 28 | impbid 211 |
. . . . 5
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅) β (ran (π β β€ β¦ (π Β· π)) β π΅ β ran (π β β€ β¦ (π Β· π)) = π΅)) |
30 | 5, 12, 29 | syl2anc 582 |
. . . 4
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (ran (π β β€ β¦ (π Β· π)) β π΅ β ran (π β β€ β¦ (π Β· π)) = π΅)) |
31 | 15, 22, 30 | 3bitr3rd 309 |
. . 3
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (ran (π β β€ β¦ (π Β· π)) = π΅ β (πβπ) = (β―βπ΅))) |
32 | 31 | pm5.32da 577 |
. 2
β’ ((πΊ β Grp β§ π΅ β Fin) β ((π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅) β (π β π΅ β§ (πβπ) = (β―βπ΅)))) |
33 | 4, 32 | bitrid 282 |
1
β’ ((πΊ β Grp β§ π΅ β Fin) β (π β πΈ β (π β π΅ β§ (πβπ) = (β―βπ΅)))) |