Step | Hyp | Ref
| Expression |
1 | | ghomlinOLD.1 |
. . . . 5
β’ π = ran πΊ |
2 | | eqid 2733 |
. . . . 5
β’ ran π» = ran π» |
3 | 1, 2 | elghomOLD 36396 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:πβΆran π» β§ βπ₯ β π βπ¦ β π ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
4 | 3 | biimp3a 1470 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉ:πβΆran π» β§ βπ₯ β π βπ¦ β π ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)))) |
5 | 4 | simprd 497 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β βπ₯ β π βπ¦ β π ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))) |
6 | | fveq2 6846 |
. . . . 5
β’ (π₯ = π΄ β (πΉβπ₯) = (πΉβπ΄)) |
7 | 6 | oveq1d 7376 |
. . . 4
β’ (π₯ = π΄ β ((πΉβπ₯)π»(πΉβπ¦)) = ((πΉβπ΄)π»(πΉβπ¦))) |
8 | | oveq1 7368 |
. . . . 5
β’ (π₯ = π΄ β (π₯πΊπ¦) = (π΄πΊπ¦)) |
9 | 8 | fveq2d 6850 |
. . . 4
β’ (π₯ = π΄ β (πΉβ(π₯πΊπ¦)) = (πΉβ(π΄πΊπ¦))) |
10 | 7, 9 | eqeq12d 2749 |
. . 3
β’ (π₯ = π΄ β (((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)) β ((πΉβπ΄)π»(πΉβπ¦)) = (πΉβ(π΄πΊπ¦)))) |
11 | | fveq2 6846 |
. . . . 5
β’ (π¦ = π΅ β (πΉβπ¦) = (πΉβπ΅)) |
12 | 11 | oveq2d 7377 |
. . . 4
β’ (π¦ = π΅ β ((πΉβπ΄)π»(πΉβπ¦)) = ((πΉβπ΄)π»(πΉβπ΅))) |
13 | | oveq2 7369 |
. . . . 5
β’ (π¦ = π΅ β (π΄πΊπ¦) = (π΄πΊπ΅)) |
14 | 13 | fveq2d 6850 |
. . . 4
β’ (π¦ = π΅ β (πΉβ(π΄πΊπ¦)) = (πΉβ(π΄πΊπ΅))) |
15 | 12, 14 | eqeq12d 2749 |
. . 3
β’ (π¦ = π΅ β (((πΉβπ΄)π»(πΉβπ¦)) = (πΉβ(π΄πΊπ¦)) β ((πΉβπ΄)π»(πΉβπ΅)) = (πΉβ(π΄πΊπ΅)))) |
16 | 10, 15 | rspc2v 3592 |
. 2
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)) β ((πΉβπ΄)π»(πΉβπ΅)) = (πΉβ(π΄πΊπ΅)))) |
17 | 5, 16 | mpan9 508 |
1
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((πΉβπ΄)π»(πΉβπ΅)) = (πΉβ(π΄πΊπ΅))) |