Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΄ β π) |
2 | | simpr2 1196 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β π΅ β π) |
3 | | grpdivf.1 |
. . . . . 6
β’ π = ran πΊ |
4 | | eqid 2733 |
. . . . . 6
β’
(invβπΊ) =
(invβπΊ) |
5 | 3, 4 | grpoinvcl 29508 |
. . . . 5
β’ ((πΊ β GrpOp β§ πΆ β π) β ((invβπΊ)βπΆ) β π) |
6 | 5 | 3ad2antr3 1191 |
. . . 4
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((invβπΊ)βπΆ) β π) |
7 | 1, 2, 6 | 3jca 1129 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) |
8 | 3 | grpoass 29487 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ ((invβπΊ)βπΆ) β π)) β ((π΄πΊπ΅)πΊ((invβπΊ)βπΆ)) = (π΄πΊ(π΅πΊ((invβπΊ)βπΆ)))) |
9 | 7, 8 | syldan 592 |
. 2
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊ((invβπΊ)βπΆ)) = (π΄πΊ(π΅πΊ((invβπΊ)βπΆ)))) |
10 | | simpl 484 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΊ β GrpOp) |
11 | 3 | grpocl 29484 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) |
12 | 11 | 3adant3r3 1185 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄πΊπ΅) β π) |
13 | | simpr3 1197 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β πΆ β π) |
14 | | grpdivf.3 |
. . . 4
β’ π· = ( /π
βπΊ) |
15 | 3, 4, 14 | grpodivval 29519 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄πΊπ΅) β π β§ πΆ β π) β ((π΄πΊπ΅)π·πΆ) = ((π΄πΊπ΅)πΊ((invβπΊ)βπΆ))) |
16 | 10, 12, 13, 15 | syl3anc 1372 |
. 2
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π·πΆ) = ((π΄πΊπ΅)πΊ((invβπΊ)βπΆ))) |
17 | 3, 4, 14 | grpodivval 29519 |
. . . 4
β’ ((πΊ β GrpOp β§ π΅ β π β§ πΆ β π) β (π΅π·πΆ) = (π΅πΊ((invβπΊ)βπΆ))) |
18 | 17 | 3adant3r1 1183 |
. . 3
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΅π·πΆ) = (π΅πΊ((invβπΊ)βπΆ))) |
19 | 18 | oveq2d 7374 |
. 2
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄πΊ(π΅π·πΆ)) = (π΄πΊ(π΅πΊ((invβπΊ)βπΆ)))) |
20 | 9, 16, 19 | 3eqtr4d 2783 |
1
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π·πΆ) = (π΄πΊ(π΅π·πΆ))) |