Step | Hyp | Ref
| Expression |
1 | | subgrcl 18934 |
. . . . . . 7
β’ (π β (SubGrpβπΊ) β πΊ β Grp) |
2 | | conjghm.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
3 | | conjghm.p |
. . . . . . . 8
β’ + =
(+gβπΊ) |
4 | | conjghm.m |
. . . . . . . 8
β’ β =
(-gβπΊ) |
5 | | eqid 2737 |
. . . . . . . 8
β’ (π₯ β π β¦ ((π΄ + π₯) β π΄)) = (π₯ β π β¦ ((π΄ + π₯) β π΄)) |
6 | 2, 3, 4, 5 | conjghm 19040 |
. . . . . . 7
β’ ((πΊ β Grp β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) β (πΊ GrpHom πΊ) β§ (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1-ontoβπ)) |
7 | 1, 6 | sylan 581 |
. . . . . 6
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) β (πΊ GrpHom πΊ) β§ (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1-ontoβπ)) |
8 | | f1of1 6784 |
. . . . . 6
β’ ((π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1-ontoβπ β (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1βπ) |
9 | 7, 8 | simpl2im 505 |
. . . . 5
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1βπ) |
10 | 2 | subgss 18930 |
. . . . . 6
β’ (π β (SubGrpβπΊ) β π β π) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π β π) |
12 | | f1ssres 6747 |
. . . . 5
β’ (((π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1βπ β§ π β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π):πβ1-1βπ) |
13 | 9, 11, 12 | syl2anc 585 |
. . . 4
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π):πβ1-1βπ) |
14 | 11 | resmptd 5995 |
. . . . . 6
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π) = (π₯ β π β¦ ((π΄ + π₯) β π΄))) |
15 | | conjsubg.f |
. . . . . 6
β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) |
16 | 14, 15 | eqtr4di 2795 |
. . . . 5
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π) = πΉ) |
17 | | f1eq1 6734 |
. . . . 5
β’ (((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π) = πΉ β (((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π):πβ1-1βπ β πΉ:πβ1-1βπ)) |
18 | 16, 17 | syl 17 |
. . . 4
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β (((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π):πβ1-1βπ β πΉ:πβ1-1βπ)) |
19 | 13, 18 | mpbid 231 |
. . 3
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β πΉ:πβ1-1βπ) |
20 | | f1f1orn 6796 |
. . 3
β’ (πΉ:πβ1-1βπ β πΉ:πβ1-1-ontoβran
πΉ) |
21 | 19, 20 | syl 17 |
. 2
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β πΉ:πβ1-1-ontoβran
πΉ) |
22 | | f1oeng 8912 |
. 2
β’ ((π β (SubGrpβπΊ) β§ πΉ:πβ1-1-ontoβran
πΉ) β π β ran πΉ) |
23 | 21, 22 | syldan 592 |
1
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π β ran πΉ) |