Step | Hyp | Ref
| Expression |
1 | | rnexg 7898 |
. . 3
β’ (πΊ β GrpOp β ran πΊ β V) |
2 | | rnexg 7898 |
. . 3
β’ (π» β GrpOp β ran π» β V) |
3 | | elghomlem1OLD.1 |
. . . 4
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} |
4 | 3 | fabexg 7928 |
. . 3
β’ ((ran
πΊ β V β§ ran π» β V) β π β V) |
5 | 1, 2, 4 | syl2an 595 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp) β π β V) |
6 | | rneq 5936 |
. . . . . 6
β’ (π = πΊ β ran π = ran πΊ) |
7 | 6 | feq2d 6704 |
. . . . 5
β’ (π = πΊ β (π:ran πβΆran β β π:ran πΊβΆran β)) |
8 | | oveq 7418 |
. . . . . . . . 9
β’ (π = πΊ β (π₯ππ¦) = (π₯πΊπ¦)) |
9 | 8 | fveq2d 6896 |
. . . . . . . 8
β’ (π = πΊ β (πβ(π₯ππ¦)) = (πβ(π₯πΊπ¦))) |
10 | 9 | eqeq2d 2742 |
. . . . . . 7
β’ (π = πΊ β (((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)) β ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
11 | 6, 10 | raleqbidv 3341 |
. . . . . 6
β’ (π = πΊ β (βπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)) β βπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
12 | 6, 11 | raleqbidv 3341 |
. . . . 5
β’ (π = πΊ β (βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
13 | 7, 12 | anbi12d 630 |
. . . 4
β’ (π = πΊ β ((π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦))) β (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦))))) |
14 | 13 | abbidv 2800 |
. . 3
β’ (π = πΊ β {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))} = {π β£ (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))}) |
15 | | rneq 5936 |
. . . . . . 7
β’ (β = π» β ran β = ran π») |
16 | 15 | feq3d 6705 |
. . . . . 6
β’ (β = π» β (π:ran πΊβΆran β β π:ran πΊβΆran π»)) |
17 | | oveq 7418 |
. . . . . . . 8
β’ (β = π» β ((πβπ₯)β(πβπ¦)) = ((πβπ₯)π»(πβπ¦))) |
18 | 17 | eqeq1d 2733 |
. . . . . . 7
β’ (β = π» β (((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)) β ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
19 | 18 | 2ralbidv 3217 |
. . . . . 6
β’ (β = π» β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))) |
20 | 16, 19 | anbi12d 630 |
. . . . 5
β’ (β = π» β ((π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦))) β (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))))) |
21 | 20 | abbidv 2800 |
. . . 4
β’ (β = π» β {π β£ (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))} = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))}) |
22 | 21, 3 | eqtr4di 2789 |
. . 3
β’ (β = π» β {π β£ (π:ran πΊβΆran β β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)β(πβπ¦)) = (πβ(π₯πΊπ¦)))} = π) |
23 | | df-ghomOLD 37056 |
. . 3
β’ GrpOpHom
= (π β GrpOp, β β GrpOp β¦ {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))}) |
24 | 14, 22, 23 | ovmpog 7570 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ π β V) β (πΊ GrpOpHom π») = π) |
25 | 5, 24 | mpd3an3 1461 |
1
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) |