Step | Hyp | Ref
| Expression |
1 | | ablogrpo 29800 |
. . 3
β’ (πΊ β AbelOp β πΊ β GrpOp) |
2 | | simpl 484 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΊ β GrpOp) |
3 | | abldiv.1 |
. . . . . 6
β’ π = ran πΊ |
4 | | abldiv.3 |
. . . . . 6
β’ π· = ( /π
βπΊ) |
5 | 3, 4 | grpodivcl 29792 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β π) |
6 | 5 | 3adant3r3 1185 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β π) |
7 | | simpr3 1197 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΆ β π) |
8 | | eqid 2733 |
. . . . 5
β’
(invβπΊ) =
(invβπΊ) |
9 | 3, 8, 4 | grpodivval 29788 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄π·π΅) β π β§ πΆ β π) β ((π΄π·π΅)π·πΆ) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
10 | 2, 6, 7, 9 | syl3anc 1372 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
11 | 1, 10 | sylan 581 |
. 2
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
12 | | simpr1 1195 |
. . . 4
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΄ β π) |
13 | | simpr2 1196 |
. . . 4
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΅ β π) |
14 | | simp3 1139 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β πΆ β π) |
15 | 3, 8 | grpoinvcl 29777 |
. . . . 5
β’ ((πΊ β GrpOp β§ πΆ β π) β ((invβπΊ)βπΆ) β π) |
16 | 1, 14, 15 | syl2an 597 |
. . . 4
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((invβπΊ)βπΆ) β π) |
17 | 12, 13, 16 | 3jca 1129 |
. . 3
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) |
18 | 3, 4 | ablodivdiv 29806 |
. . 3
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) β (π΄π·(π΅π·((invβπΊ)βπΆ))) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
19 | 17, 18 | syldan 592 |
. 2
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·((invβπΊ)βπΆ))) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
20 | 3, 8, 4 | grpodivinv 29789 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΅ β π β§ πΆ β π) β (π΅π·((invβπΊ)βπΆ)) = (π΅πΊπΆ)) |
21 | 1, 20 | syl3an1 1164 |
. . . 4
β’ ((πΊ β AbelOp β§ π΅ β π β§ πΆ β π) β (π΅π·((invβπΊ)βπΆ)) = (π΅πΊπΆ)) |
22 | 21 | 3adant3r1 1183 |
. . 3
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·((invβπΊ)βπΆ)) = (π΅πΊπΆ)) |
23 | 22 | oveq2d 7425 |
. 2
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·((invβπΊ)βπΆ))) = (π΄π·(π΅πΊπΆ))) |
24 | 11, 19, 23 | 3eqtr2d 2779 |
1
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = (π΄π·(π΅πΊπΆ))) |