Step | Hyp | Ref
| Expression |
1 | | ablogrpo 29787 |
. . 3
β’ (πΊ β AbelOp β πΊ β GrpOp) |
2 | | simpl 483 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΊ β GrpOp) |
3 | | abldiv.1 |
. . . . . 6
β’ π = ran πΊ |
4 | | abldiv.3 |
. . . . . 6
β’ π· = ( /π
βπΊ) |
5 | 3, 4 | grpodivcl 29779 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β π) |
6 | 5 | 3adant3r3 1184 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β π) |
7 | | simpr3 1196 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΆ β π) |
8 | | eqid 2732 |
. . . . 5
β’
(invβπΊ) =
(invβπΊ) |
9 | 3, 8, 4 | grpodivval 29775 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄π·π΅) β π β§ πΆ β π) β ((π΄π·π΅)π·πΆ) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
10 | 2, 6, 7, 9 | syl3anc 1371 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
11 | 1, 10 | sylan 580 |
. 2
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
12 | | simpr1 1194 |
. . . 4
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΄ β π) |
13 | | simpr2 1195 |
. . . 4
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΅ β π) |
14 | | simp3 1138 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β πΆ β π) |
15 | 3, 8 | grpoinvcl 29764 |
. . . . 5
β’ ((πΊ β GrpOp β§ πΆ β π) β ((invβπΊ)βπΆ) β π) |
16 | 1, 14, 15 | syl2an 596 |
. . . 4
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((invβπΊ)βπΆ) β π) |
17 | 12, 13, 16 | 3jca 1128 |
. . 3
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) |
18 | 3, 4 | ablodivdiv 29793 |
. . 3
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) β (π΄π·(π΅π·((invβπΊ)βπΆ))) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
19 | 17, 18 | syldan 591 |
. 2
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·((invβπΊ)βπΆ))) = ((π΄π·π΅)πΊ((invβπΊ)βπΆ))) |
20 | 3, 8, 4 | grpodivinv 29776 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΅ β π β§ πΆ β π) β (π΅π·((invβπΊ)βπΆ)) = (π΅πΊπΆ)) |
21 | 1, 20 | syl3an1 1163 |
. . . 4
β’ ((πΊ β AbelOp β§ π΅ β π β§ πΆ β π) β (π΅π·((invβπΊ)βπΆ)) = (π΅πΊπΆ)) |
22 | 21 | 3adant3r1 1182 |
. . 3
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·((invβπΊ)βπΆ)) = (π΅πΊπΆ)) |
23 | 22 | oveq2d 7421 |
. 2
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·(π΅π·((invβπΊ)βπΆ))) = (π΄π·(π΅πΊπΆ))) |
24 | 11, 19, 23 | 3eqtr2d 2778 |
1
β’ ((πΊ β AbelOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π·πΆ) = (π΄π·(π΅πΊπΆ))) |