Step | Hyp | Ref
| Expression |
1 | | subgrcl 19058 |
. . . . . . 7
β’ (π β (SubGrpβπΊ) β πΊ β Grp) |
2 | | conjghm.x |
. . . . . . . 8
β’ π = (BaseβπΊ) |
3 | | conjghm.p |
. . . . . . . 8
β’ + =
(+gβπΊ) |
4 | | conjghm.m |
. . . . . . . 8
β’ β =
(-gβπΊ) |
5 | | eqid 2726 |
. . . . . . . 8
β’ (π₯ β π β¦ ((π΄ + π₯) β π΄)) = (π₯ β π β¦ ((π΄ + π₯) β π΄)) |
6 | 2, 3, 4, 5 | conjghm 19174 |
. . . . . . 7
β’ ((πΊ β Grp β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) β (πΊ GrpHom πΊ) β§ (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1-ontoβπ)) |
7 | 1, 6 | sylan 579 |
. . . . . 6
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) β (πΊ GrpHom πΊ) β§ (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1-ontoβπ)) |
8 | | f1of1 6826 |
. . . . . 6
β’ ((π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1-ontoβπ β (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1βπ) |
9 | 7, 8 | simpl2im 503 |
. . . . 5
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β (π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1βπ) |
10 | 2 | subgss 19054 |
. . . . . 6
β’ (π β (SubGrpβπΊ) β π β π) |
11 | 10 | adantr 480 |
. . . . 5
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π β π) |
12 | | f1ssres 6789 |
. . . . 5
β’ (((π₯ β π β¦ ((π΄ + π₯) β π΄)):πβ1-1βπ β§ π β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π):πβ1-1βπ) |
13 | 9, 11, 12 | syl2anc 583 |
. . . 4
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π):πβ1-1βπ) |
14 | 11 | resmptd 6034 |
. . . . . 6
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π) = (π₯ β π β¦ ((π΄ + π₯) β π΄))) |
15 | | conjsubg.f |
. . . . . 6
β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) |
16 | 14, 15 | eqtr4di 2784 |
. . . . 5
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ((π₯ β π β¦ ((π΄ + π₯) β π΄)) βΎ π) = πΉ) |
17 | | f1eq1 6776 |
. . . . 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 6838 |
. . 3
β’ (πΉ:πβ1-1βπ β πΉ:πβ1-1-ontoβran
πΉ) |
21 | 19, 20 | syl 17 |
. 2
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β πΉ:πβ1-1-ontoβran
πΉ) |
22 | | f1oeng 8969 |
. 2
β’ ((π β (SubGrpβπΊ) β§ πΉ:πβ1-1-ontoβran
πΉ) β π β ran πΉ) |
23 | 21, 22 | syldan 590 |
1
β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π β ran πΉ) |