Step | Hyp | Ref
| Expression |
1 | | elghomlem1OLD.1 |
. . . 4
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} |
2 | 1 | elghomlem1OLD 36282 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) |
3 | 2 | eleq2d 2823 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β πΉ β π)) |
4 | | elex 3461 |
. . . . 5
β’ (πΉ β π β πΉ β V) |
5 | | feq1 6646 |
. . . . . . . 8
β’ (π = πΉ β (π:ran πΊβΆran π» β πΉ:ran πΊβΆran π»)) |
6 | | fveq1 6838 |
. . . . . . . . . . 11
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
7 | | fveq1 6838 |
. . . . . . . . . . 11
β’ (π = πΉ β (πβπ¦) = (πΉβπ¦)) |
8 | 6, 7 | oveq12d 7369 |
. . . . . . . . . 10
β’ (π = πΉ β ((πβπ₯)π»(πβπ¦)) = ((πΉβπ₯)π»(πΉβπ¦))) |
9 | | fveq1 6838 |
. . . . . . . . . 10
β’ (π = πΉ β (πβ(π₯πΊπ¦)) = (πΉβ(π₯πΊπ¦))) |
10 | 8, 9 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π = πΉ β (((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)))) |
11 | 10 | 2ralbidv 3210 |
. . . . . . . 8
β’ (π = πΉ β (βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)) β βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)))) |
12 | 5, 11 | anbi12d 631 |
. . . . . . 7
β’ (π = πΉ β ((π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦))) β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
13 | 12, 1 | elab2g 3630 |
. . . . . 6
β’ (πΉ β V β (πΉ β π β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
14 | 13 | biimpd 228 |
. . . . 5
β’ (πΉ β V β (πΉ β π β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
15 | 4, 14 | mpcom 38 |
. . . 4
β’ (πΉ β π β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)))) |
16 | | rnexg 7833 |
. . . . . . 7
β’ (πΊ β GrpOp β ran πΊ β V) |
17 | | fex 7172 |
. . . . . . . 8
β’ ((πΉ:ran πΊβΆran π» β§ ran πΊ β V) β πΉ β V) |
18 | 17 | expcom 414 |
. . . . . . 7
β’ (ran
πΊ β V β (πΉ:ran πΊβΆran π» β πΉ β V)) |
19 | 16, 18 | syl 17 |
. . . . . 6
β’ (πΊ β GrpOp β (πΉ:ran πΊβΆran π» β πΉ β V)) |
20 | 19 | adantrd 492 |
. . . . 5
β’ (πΊ β GrpOp β ((πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))) β πΉ β V)) |
21 | 13 | biimprd 247 |
. . . . 5
β’ (πΉ β V β ((πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))) β πΉ β π)) |
22 | 20, 21 | syli 39 |
. . . 4
β’ (πΊ β GrpOp β ((πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))) β πΉ β π)) |
23 | 15, 22 | impbid2 225 |
. . 3
β’ (πΊ β GrpOp β (πΉ β π β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
24 | 23 | adantr 481 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β π β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
25 | 3, 24 | bitrd 278 |
1
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |