Step | Hyp | Ref
| Expression |
1 | | grpinv.1 |
. . . . . 6
β’ π = ran πΊ |
2 | | grpinv.2 |
. . . . . 6
β’ π = (GIdβπΊ) |
3 | | grpinv.3 |
. . . . . 6
β’ π = (invβπΊ) |
4 | 1, 2, 3 | grpoinvval 29776 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π) β (πβπ΄) = (β©π¦ β π (π¦πΊπ΄) = π)) |
5 | 1, 2 | grpoinveu 29772 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΄ β π) β β!π¦ β π (π¦πΊπ΄) = π) |
6 | | riotacl2 7382 |
. . . . . 6
β’
(β!π¦ β
π (π¦πΊπ΄) = π β (β©π¦ β π (π¦πΊπ΄) = π) β {π¦ β π β£ (π¦πΊπ΄) = π}) |
7 | 5, 6 | syl 17 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π) β (β©π¦ β π (π¦πΊπ΄) = π) β {π¦ β π β£ (π¦πΊπ΄) = π}) |
8 | 4, 7 | eqeltrd 2834 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π) β (πβπ΄) β {π¦ β π β£ (π¦πΊπ΄) = π}) |
9 | | simpl 484 |
. . . . . . . . 9
β’ (((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β (π¦πΊπ΄) = π) |
10 | 9 | rgenw 3066 |
. . . . . . . 8
β’
βπ¦ β
π (((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β (π¦πΊπ΄) = π) |
11 | 10 | a1i 11 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π΄ β π) β βπ¦ β π (((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β (π¦πΊπ΄) = π)) |
12 | 1, 2 | grpoidinv2 29768 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ π΄ β π) β (((ππΊπ΄) = π΄ β§ (π΄πΊπ) = π΄) β§ βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π))) |
13 | 12 | simprd 497 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π΄ β π) β βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)) |
14 | 11, 13, 5 | 3jca 1129 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΄ β π) β (βπ¦ β π (((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β (π¦πΊπ΄) = π) β§ βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β§ β!π¦ β π (π¦πΊπ΄) = π)) |
15 | | reupick2 4321 |
. . . . . 6
β’
(((βπ¦ β
π (((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β (π¦πΊπ΄) = π) β§ βπ¦ β π ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β§ β!π¦ β π (π¦πΊπ΄) = π) β§ π¦ β π) β ((π¦πΊπ΄) = π β ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π))) |
16 | 14, 15 | sylan 581 |
. . . . 5
β’ (((πΊ β GrpOp β§ π΄ β π) β§ π¦ β π) β ((π¦πΊπ΄) = π β ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π))) |
17 | 16 | rabbidva 3440 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π) β {π¦ β π β£ (π¦πΊπ΄) = π} = {π¦ β π β£ ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)}) |
18 | 8, 17 | eleqtrd 2836 |
. . 3
β’ ((πΊ β GrpOp β§ π΄ β π) β (πβπ΄) β {π¦ β π β£ ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)}) |
19 | | oveq1 7416 |
. . . . . 6
β’ (π¦ = (πβπ΄) β (π¦πΊπ΄) = ((πβπ΄)πΊπ΄)) |
20 | 19 | eqeq1d 2735 |
. . . . 5
β’ (π¦ = (πβπ΄) β ((π¦πΊπ΄) = π β ((πβπ΄)πΊπ΄) = π)) |
21 | | oveq2 7417 |
. . . . . 6
β’ (π¦ = (πβπ΄) β (π΄πΊπ¦) = (π΄πΊ(πβπ΄))) |
22 | 21 | eqeq1d 2735 |
. . . . 5
β’ (π¦ = (πβπ΄) β ((π΄πΊπ¦) = π β (π΄πΊ(πβπ΄)) = π)) |
23 | 20, 22 | anbi12d 632 |
. . . 4
β’ (π¦ = (πβπ΄) β (((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π) β (((πβπ΄)πΊπ΄) = π β§ (π΄πΊ(πβπ΄)) = π))) |
24 | 23 | elrab 3684 |
. . 3
β’ ((πβπ΄) β {π¦ β π β£ ((π¦πΊπ΄) = π β§ (π΄πΊπ¦) = π)} β ((πβπ΄) β π β§ (((πβπ΄)πΊπ΄) = π β§ (π΄πΊ(πβπ΄)) = π))) |
25 | 18, 24 | sylib 217 |
. 2
β’ ((πΊ β GrpOp β§ π΄ β π) β ((πβπ΄) β π β§ (((πβπ΄)πΊπ΄) = π β§ (π΄πΊ(πβπ΄)) = π))) |
26 | 25 | simprd 497 |
1
β’ ((πΊ β GrpOp β§ π΄ β π) β (((πβπ΄)πΊπ΄) = π β§ (π΄πΊ(πβπ΄)) = π)) |