Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β π» β GrpOp) |
2 | | ghomdiv.1 |
. . . . . . 7
β’ π = ran πΊ |
3 | | eqid 2733 |
. . . . . . 7
β’ ran π» = ran π» |
4 | 2, 3 | ghomf 36399 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:πβΆran π») |
5 | 4 | ffvelcdmda 7039 |
. . . . 5
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ π΄ β π) β (πΉβπ΄) β ran π») |
6 | 5 | adantrr 716 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΄) β ran π») |
7 | 4 | ffvelcdmda 7039 |
. . . . 5
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ π΅ β π) β (πΉβπ΅) β ran π») |
8 | 7 | adantrl 715 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β ran π») |
9 | | ghomdiv.3 |
. . . . 5
β’ πΆ = ( /π
βπ») |
10 | 3, 9 | grponpcan 29534 |
. . . 4
β’ ((π» β GrpOp β§ (πΉβπ΄) β ran π» β§ (πΉβπ΅) β ran π») β (((πΉβπ΄)πΆ(πΉβπ΅))π»(πΉβπ΅)) = (πΉβπ΄)) |
11 | 1, 6, 8, 10 | syl3anc 1372 |
. . 3
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (((πΉβπ΄)πΆ(πΉβπ΅))π»(πΉβπ΅)) = (πΉβπ΄)) |
12 | | ghomdiv.2 |
. . . . . . 7
β’ π· = ( /π
βπΊ) |
13 | 2, 12 | grponpcan 29534 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅)πΊπ΅) = π΄) |
14 | 13 | 3expb 1121 |
. . . . 5
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β ((π΄π·π΅)πΊπ΅) = π΄) |
15 | 14 | 3ad2antl1 1186 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((π΄π·π΅)πΊπ΅) = π΄) |
16 | 15 | fveq2d 6850 |
. . 3
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ((π΄π·π΅)πΊπ΅)) = (πΉβπ΄)) |
17 | 2, 12 | grpodivcl 29530 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β π) |
18 | 17 | 3expb 1121 |
. . . . . 6
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β (π΄π·π΅) β π) |
19 | | simprr 772 |
. . . . . 6
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
20 | 18, 19 | jca 513 |
. . . . 5
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β ((π΄π·π΅) β π β§ π΅ β π)) |
21 | 20 | 3ad2antl1 1186 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((π΄π·π΅) β π β§ π΅ β π)) |
22 | 2 | ghomlinOLD 36397 |
. . . . 5
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ ((π΄π·π΅) β π β§ π΅ β π)) β ((πΉβ(π΄π·π΅))π»(πΉβπ΅)) = (πΉβ((π΄π·π΅)πΊπ΅))) |
23 | 22 | eqcomd 2739 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ ((π΄π·π΅) β π β§ π΅ β π)) β (πΉβ((π΄π·π΅)πΊπ΅)) = ((πΉβ(π΄π·π΅))π»(πΉβπ΅))) |
24 | 21, 23 | syldan 592 |
. . 3
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ((π΄π·π΅)πΊπ΅)) = ((πΉβ(π΄π·π΅))π»(πΉβπ΅))) |
25 | 11, 16, 24 | 3eqtr2rd 2780 |
. 2
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((πΉβ(π΄π·π΅))π»(πΉβπ΅)) = (((πΉβπ΄)πΆ(πΉβπ΅))π»(πΉβπ΅))) |
26 | 18 | 3ad2antl1 1186 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (π΄π·π΅) β π) |
27 | 4 | ffvelcdmda 7039 |
. . . 4
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄π·π΅) β π) β (πΉβ(π΄π·π΅)) β ran π») |
28 | 26, 27 | syldan 592 |
. . 3
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π·π΅)) β ran π») |
29 | 3, 9 | grpodivcl 29530 |
. . . 4
β’ ((π» β GrpOp β§ (πΉβπ΄) β ran π» β§ (πΉβπ΅) β ran π») β ((πΉβπ΄)πΆ(πΉβπ΅)) β ran π») |
30 | 1, 6, 8, 29 | syl3anc 1372 |
. . 3
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((πΉβπ΄)πΆ(πΉβπ΅)) β ran π») |
31 | 3 | grporcan 29509 |
. . 3
β’ ((π» β GrpOp β§ ((πΉβ(π΄π·π΅)) β ran π» β§ ((πΉβπ΄)πΆ(πΉβπ΅)) β ran π» β§ (πΉβπ΅) β ran π»)) β (((πΉβ(π΄π·π΅))π»(πΉβπ΅)) = (((πΉβπ΄)πΆ(πΉβπ΅))π»(πΉβπ΅)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅)))) |
32 | 1, 28, 30, 8, 31 | syl13anc 1373 |
. 2
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (((πΉβ(π΄π·π΅))π»(πΉβπ΅)) = (((πΉβπ΄)πΆ(πΉβπ΅))π»(πΉβπ΅)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅)))) |
33 | 25, 32 | mpbid 231 |
1
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅))) |