Step | Hyp | Ref
| Expression |
1 | | eqid 2725 |
. . . . . . 7
β’ ran πΊ = ran πΊ |
2 | | ghomidOLD.1 |
. . . . . . 7
β’ π = (GIdβπΊ) |
3 | 1, 2 | grpoidcl 30368 |
. . . . . 6
β’ (πΊ β GrpOp β π β ran πΊ) |
4 | 3 | 3ad2ant1 1130 |
. . . . 5
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β π β ran πΊ) |
5 | 4, 4 | jca 510 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (π β ran πΊ β§ π β ran πΊ)) |
6 | 1 | ghomlinOLD 37418 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π β ran πΊ β§ π β ran πΊ)) β ((πΉβπ)π»(πΉβπ)) = (πΉβ(ππΊπ))) |
7 | 5, 6 | mpdan 685 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β ((πΉβπ)π»(πΉβπ)) = (πΉβ(ππΊπ))) |
8 | 1, 2 | grpolid 30370 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π β ran πΊ) β (ππΊπ) = π) |
9 | 3, 8 | mpdan 685 |
. . . . 5
β’ (πΊ β GrpOp β (ππΊπ) = π) |
10 | 9 | fveq2d 6896 |
. . . 4
β’ (πΊ β GrpOp β (πΉβ(ππΊπ)) = (πΉβπ)) |
11 | 10 | 3ad2ant1 1130 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβ(ππΊπ)) = (πΉβπ)) |
12 | 7, 11 | eqtrd 2765 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β ((πΉβπ)π»(πΉβπ)) = (πΉβπ)) |
13 | | eqid 2725 |
. . . . . . 7
β’ ran π» = ran π» |
14 | 1, 13 | elghomOLD 37417 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
15 | 14 | biimp3a 1465 |
. . . . 5
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)))) |
16 | 15 | simpld 493 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:ran πΊβΆran π») |
17 | 16, 4 | ffvelcdmd 7090 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβπ) β ran π») |
18 | | ghomidOLD.2 |
. . . . . 6
β’ π = (GIdβπ») |
19 | 13, 18 | grpoid 30374 |
. . . . 5
β’ ((π» β GrpOp β§ (πΉβπ) β ran π») β ((πΉβπ) = π β ((πΉβπ)π»(πΉβπ)) = (πΉβπ))) |
20 | 19 | ex 411 |
. . . 4
β’ (π» β GrpOp β ((πΉβπ) β ran π» β ((πΉβπ) = π β ((πΉβπ)π»(πΉβπ)) = (πΉβπ)))) |
21 | 20 | 3ad2ant2 1131 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β ((πΉβπ) β ran π» β ((πΉβπ) = π β ((πΉβπ)π»(πΉβπ)) = (πΉβπ)))) |
22 | 17, 21 | mpd 15 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β ((πΉβπ) = π β ((πΉβπ)π»(πΉβπ)) = (πΉβπ))) |
23 | 12, 22 | mpbird 256 |
1
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβπ) = π) |