Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . . . . 7
β’ ran πΊ = ran πΊ |
2 | | ghomidOLD.1 |
. . . . . . 7
β’ π = (GIdβπΊ) |
3 | 1, 2 | grpoidcl 30276 |
. . . . . 6
β’ (πΊ β GrpOp β π β ran πΊ) |
4 | 3 | 3ad2ant1 1130 |
. . . . 5
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β π β ran πΊ) |
5 | 4, 4 | jca 511 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (π β ran πΊ β§ π β ran πΊ)) |
6 | 1 | ghomlinOLD 37269 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π β ran πΊ β§ π β ran πΊ)) β ((πΉβπ)π»(πΉβπ)) = (πΉβ(ππΊπ))) |
7 | 5, 6 | mpdan 684 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β ((πΉβπ)π»(πΉβπ)) = (πΉβ(ππΊπ))) |
8 | 1, 2 | grpolid 30278 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π β ran πΊ) β (ππΊπ) = π) |
9 | 3, 8 | mpdan 684 |
. . . . 5
β’ (πΊ β GrpOp β (ππΊπ) = π) |
10 | 9 | fveq2d 6889 |
. . . 4
β’ (πΊ β GrpOp β (πΉβ(ππΊπ)) = (πΉβπ)) |
11 | 10 | 3ad2ant1 1130 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβ(ππΊπ)) = (πΉβπ)) |
12 | 7, 11 | eqtrd 2766 |
. 2
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β ((πΉβπ)π»(πΉβπ)) = (πΉβπ)) |
13 | | eqid 2726 |
. . . . . . 7
β’ ran π» = ran π» |
14 | 1, 13 | elghomOLD 37268 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) |
15 | 14 | biimp3a 1465 |
. . . . 5
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦)))) |
16 | 15 | simpld 494 |
. . . 4
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:ran πΊβΆran π») |
17 | 16, 4 | ffvelcdmd 7081 |
. . 3
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβπ) β ran π») |
18 | | ghomidOLD.2 |
. . . . . 6
β’ π = (GIdβπ») |
19 | 13, 18 | grpoid 30282 |
. . . . 5
β’ ((π» β GrpOp β§ (πΉβπ) β ran π») β ((πΉβπ) = π β ((πΉβπ)π»(πΉβπ)) = (πΉβπ))) |
20 | 19 | ex 412 |
. . . 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 257 |
1
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβπ) = π) |