Step | Hyp | Ref
| Expression |
1 | | cayley.x |
. . . 4
β’ π = (BaseβπΊ) |
2 | | cayley.h |
. . . 4
β’ π» = (SymGrpβπ) |
3 | | eqid 2733 |
. . . 4
β’
(+gβπΊ) = (+gβπΊ) |
4 | | eqid 2733 |
. . . 4
β’ (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) = (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) |
5 | | eqid 2733 |
. . . 4
β’ ran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))) = ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) |
6 | 1, 2, 3, 4, 5 | cayley 19201 |
. . 3
β’ (πΊ β Grp β (ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (SubGrpβπ») β§ (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) β§ (π β π β¦ (π β π β¦ (π(+gβπΊ)π))):πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) |
7 | 6 | simp1d 1143 |
. 2
β’ (πΊ β Grp β ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (SubGrpβπ»)) |
8 | 6 | simp2d 1144 |
. . 3
β’ (πΊ β Grp β (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π)))))) |
9 | 6 | simp3d 1145 |
. . 3
β’ (πΊ β Grp β (π β π β¦ (π β π β¦ (π(+gβπΊ)π))):πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π)))) |
10 | | f1oeq1 6773 |
. . . 4
β’ (π = (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (π:πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (π β π β¦ (π β π β¦ (π(+gβπΊ)π))):πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) |
11 | 10 | rspcev 3580 |
. . 3
β’ (((π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) β§ (π β π β¦ (π β π β¦ (π(+gβπΊ)π))):πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π)))) β βπ β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π)))))π:πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π)))) |
12 | 8, 9, 11 | syl2anc 585 |
. 2
β’ (πΊ β Grp β βπ β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π)))))π:πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π)))) |
13 | | oveq2 7366 |
. . . . 5
β’ (π = ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (π» βΎs π ) = (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) |
14 | 13 | oveq2d 7374 |
. . . 4
β’ (π = ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (πΊ GrpHom (π» βΎs π )) = (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π)))))) |
15 | | f1oeq3 6775 |
. . . 4
β’ (π = ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (π:πβ1-1-ontoβπ β π:πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) |
16 | 14, 15 | rexeqbidv 3319 |
. . 3
β’ (π = ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (βπ β (πΊ GrpHom (π» βΎs π ))π:πβ1-1-ontoβπ β βπ β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π)))))π:πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))))) |
17 | 16 | rspcev 3580 |
. 2
β’ ((ran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π))) β (SubGrpβπ») β§ βπ β (πΊ GrpHom (π» βΎs ran (π β π β¦ (π β π β¦ (π(+gβπΊ)π)))))π:πβ1-1-ontoβran
(π β π β¦ (π β π β¦ (π(+gβπΊ)π)))) β βπ β (SubGrpβπ»)βπ β (πΊ GrpHom (π» βΎs π ))π:πβ1-1-ontoβπ ) |
18 | 7, 12, 17 | syl2anc 585 |
1
β’ (πΊ β Grp β βπ β (SubGrpβπ»)βπ β (πΊ GrpHom (π» βΎs π ))π:πβ1-1-ontoβπ ) |