Step | Hyp | Ref
| Expression |
1 | | iscyg.1 |
. . 3
β’ π΅ = (BaseβπΊ) |
2 | | iscyg.2 |
. . 3
β’ Β· =
(.gβπΊ) |
3 | | iscyg3.e |
. . 3
β’ πΈ = {π₯ β π΅ β£ ran (π β β€ β¦ (π Β· π₯)) = π΅} |
4 | 1, 2, 3 | iscyggen 19800 |
. 2
β’ (π β πΈ β (π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅)) |
5 | | simplr 766 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β π΅ β Fin) |
6 | | simplll 772 |
. . . . . . . . 9
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β πΊ β Grp) |
7 | | simpr 484 |
. . . . . . . . 9
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β π β β€) |
8 | | simplr 766 |
. . . . . . . . 9
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β π β π΅) |
9 | 1, 2 | mulgcl 19018 |
. . . . . . . . 9
β’ ((πΊ β Grp β§ π β β€ β§ π β π΅) β (π Β· π) β π΅) |
10 | 6, 7, 8, 9 | syl3anc 1368 |
. . . . . . . 8
β’ ((((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β§ π β β€) β (π Β· π) β π΅) |
11 | 10 | fmpttd 7110 |
. . . . . . 7
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (π β β€ β¦ (π Β· π)):β€βΆπ΅) |
12 | 11 | frnd 6719 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ran (π β β€ β¦ (π Β· π)) β π΅) |
13 | 5, 12 | ssfid 9269 |
. . . . 5
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ran (π β β€ β¦ (π Β· π)) β Fin) |
14 | | hashen 14312 |
. . . . 5
β’ ((ran
(π β β€ β¦
(π Β· π)) β Fin β§ π΅ β Fin) β ((β―βran
(π β β€ β¦
(π Β· π))) = (β―βπ΅) β ran (π β β€ β¦ (π Β· π)) β π΅)) |
15 | 13, 5, 14 | syl2anc 583 |
. . . 4
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ((β―βran (π β β€ β¦ (π Β· π))) = (β―βπ΅) β ran (π β β€ β¦ (π Β· π)) β π΅)) |
16 | | cyggenod.o |
. . . . . . . 8
β’ π = (odβπΊ) |
17 | | eqid 2726 |
. . . . . . . 8
β’ (π β β€ β¦ (π Β· π)) = (π β β€ β¦ (π Β· π)) |
18 | 1, 16, 2, 17 | dfod2 19484 |
. . . . . . 7
β’ ((πΊ β Grp β§ π β π΅) β (πβπ) = if(ran (π β β€ β¦ (π Β· π)) β Fin, (β―βran (π β β€ β¦ (π Β· π))), 0)) |
19 | 18 | adantlr 712 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (πβπ) = if(ran (π β β€ β¦ (π Β· π)) β Fin, (β―βran (π β β€ β¦ (π Β· π))), 0)) |
20 | 13 | iftrued 4531 |
. . . . . 6
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β if(ran (π β β€ β¦ (π Β· π)) β Fin, (β―βran (π β β€ β¦ (π Β· π))), 0) = (β―βran (π β β€ β¦ (π Β· π)))) |
21 | 19, 20 | eqtr2d 2767 |
. . . . 5
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (β―βran (π β β€ β¦ (π Β· π))) = (πβπ)) |
22 | 21 | eqeq1d 2728 |
. . . 4
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β ((β―βran (π β β€ β¦ (π Β· π))) = (β―βπ΅) β (πβπ) = (β―βπ΅))) |
23 | | fisseneq 9259 |
. . . . . . 7
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅ β§ ran (π β β€ β¦ (π Β· π)) β π΅) β ran (π β β€ β¦ (π Β· π)) = π΅) |
24 | 23 | 3expia 1118 |
. . . . . 6
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅) β (ran (π β β€ β¦ (π Β· π)) β π΅ β ran (π β β€ β¦ (π Β· π)) = π΅)) |
25 | | enrefg 8982 |
. . . . . . . 8
β’ (π΅ β Fin β π΅ β π΅) |
26 | 25 | adantr 480 |
. . . . . . 7
β’ ((π΅ β Fin β§ ran (π β β€ β¦ (π Β· π)) β π΅) β π΅ β π΅) |
27 | | breq1 5144 |
. . . . . . 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 583 |
. . . 4
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (ran (π β β€ β¦ (π Β· π)) β π΅ β ran (π β β€ β¦ (π Β· π)) = π΅)) |
31 | 15, 22, 30 | 3bitr3rd 310 |
. . 3
β’ (((πΊ β Grp β§ π΅ β Fin) β§ π β π΅) β (ran (π β β€ β¦ (π Β· π)) = π΅ β (πβπ) = (β―βπ΅))) |
32 | 31 | pm5.32da 578 |
. 2
β’ ((πΊ β Grp β§ π΅ β Fin) β ((π β π΅ β§ ran (π β β€ β¦ (π Β· π)) = π΅) β (π β π΅ β§ (πβπ) = (β―βπ΅)))) |
33 | 4, 32 | bitrid 283 |
1
β’ ((πΊ β Grp β§ π΅ β Fin) β (π β πΈ β (π β π΅ β§ (πβπ) = (β―βπ΅)))) |