Step | Hyp | Ref
| Expression |
1 | | rnexg 7845 |
. . 3
β’ (πΊ β GrpOp β ran πΊ β V) |
2 | | rnexg 7845 |
. . 3
β’ (π» β GrpOp β ran π» β V) |
3 | | elghomlem1OLD.1 |
. . . 4
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} |
4 | 3 | fabexg 7875 |
. . 3
β’ ((ran
πΊ β V β§ ran π» β V) β π β V) |
5 | 1, 2, 4 | syl2an 597 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp) β π β V) |
6 | | rneq 5895 |
. . . . . 6
β’ (π = πΊ β ran π = ran πΊ) |
7 | 6 | feq2d 6658 |
. . . . 5
β’ (π = πΊ β (π:ran πβΆran β β π:ran πΊβΆran β)) |
8 | | oveq 7367 |
. . . . . . . . 9
β’ (π = πΊ β (π₯ππ¦) = (π₯πΊπ¦)) |
9 | 8 | fveq2d 6850 |
. . . . . . . 8
β’ (π = πΊ β (πβ(π₯ππ¦)) = (πβ(π₯πΊπ¦))) |
10 | 9 | eqeq2d 2744 |
. . . . . . 7
β’ (π = πΊ β (((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)) β ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
11 | 6, 10 | raleqbidv 3318 |
. . . . . 6
β’ (π = πΊ β (βπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)) β βπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
12 | 6, 11 | raleqbidv 3318 |
. . . . 5
β’ (π = πΊ β (βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
13 | 7, 12 | anbi12d 632 |
. . . 4
β’ (π = πΊ β ((π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦))) β (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦))))) |
14 | 13 | abbidv 2802 |
. . 3
β’ (π = πΊ β {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))} = {π β£ (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))}) |
15 | | rneq 5895 |
. . . . . . 7
β’ (β = π» β ran β = ran π») |
16 | 15 | feq3d 6659 |
. . . . . 6
β’ (β = π» β (π:ran πΊβΆran β β π:ran πΊβΆran π»)) |
17 | | oveq 7367 |
. . . . . . . 8
β’ (β = π» β ((πβπ₯)β(πβπ¦)) = ((πβπ₯)π»(πβπ¦))) |
18 | 17 | eqeq1d 2735 |
. . . . . . 7
β’ (β = π» β (((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)) β ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
19 | 18 | 2ralbidv 3209 |
. . . . . 6
β’ (β = π» β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
20 | 16, 19 | anbi12d 632 |
. . . . 5
β’ (β = π» β ((π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦))) β (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))))) |
21 | 20 | abbidv 2802 |
. . . 4
β’ (β = π» β {π β£ (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))} = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))}) |
22 | 21, 3 | eqtr4di 2791 |
. . 3
β’ (β = π» β {π β£ (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))} = π) |
23 | | df-ghomOLD 36393 |
. . 3
β’ GrpOpHom
= (π β GrpOp, β β GrpOp β¦ {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))}) |
24 | 14, 22, 23 | ovmpog 7518 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ π β V) β (πΊ GrpOpHom π») = π) |
25 | 5, 24 | mpd3an3 1463 |
1
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) |