| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Mapping of the inverse function of a group. |
| Ref | Expression |
|---|---|
| grpasscan1.1 |
|
| grpasscan1.2 |
|
| Ref | Expression |
|---|---|
| grpinvf |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rnexg 4207 |
. . . . . . . . . 10
| |
| 2 | grpasscan1.1 |
. . . . . . . . . 10
| |
| 3 | 1, 2 | syl5eqel 1975 |
. . . . . . . . 9
|
| 4 | rabexg 3460 |
. . . . . . . . 9
| |
| 5 | 3, 4 | syl 12 |
. . . . . . . 8
|
| 6 | uniexg 3795 |
. . . . . . . 8
| |
| 7 | 5, 6 | syl 12 |
. . . . . . 7
|
| 8 | 7 | adantr 425 |
. . . . . 6
|
| 9 | 8 | r19.21aiva 2176 |
. . . . 5
|
| 10 | eqid 1884 |
. . . . . 6
| |
| 11 | 10 | fnopab2g 4547 |
. . . . 5
|
| 12 | 9, 11 | sylib 215 |
. . . 4
|
| 13 | eqid 1884 |
. . . . . 6
| |
| 14 | grpasscan1.2 |
. . . . . 6
| |
| 15 | 2, 13, 14 | grpinvfval 9350 |
. . . . 5
|
| 16 | 15 | fneq1d 4505 |
. . . 4
|
| 17 | 12, 16 | mpbird 213 |
. . 3
|
| 18 | fnrnfv 4718 |
. . . . 5
| |
| 19 | 17, 18 | syl 12 |
. . . 4
|
| 20 | 2, 14 | grpinvcl 9352 |
. . . . . . . 8
|
| 21 | 2, 14 | grp2inv 9363 |
. . . . . . . . 9
|
| 22 | 21 | eqcomd 1889 |
. . . . . . . 8
|
| 23 | fveq2 4681 |
. . . . . . . . . 10
| |
| 24 | 23 | eqeq2d 1895 |
. . . . . . . . 9
|
| 25 | 24 | rcla4ev 2381 |
. . . . . . . 8
|
| 26 | 20, 22, 25 | syl11anc 524 |
. . . . . . 7
|
| 27 | 26 | ex 402 |
. . . . . 6
|
| 28 | simpr 350 |
. . . . . . . . 9
| |
| 29 | 2, 14 | grpinvcl 9352 |
. . . . . . . . . 10
|
| 30 | 29 | adantr 425 |
. . . . . . . . 9
|
| 31 | 28, 30 | eqeltrd 1971 |
. . . . . . . 8
|
| 32 | 31 | exp31 407 |
. . . . . . 7
|
| 33 | 32 | r19.23adv 2215 |
. . . . . 6
|
| 34 | 27, 33 | impbid 574 |
. . . . 5
|
| 35 | 34 | abbi2dv 2009 |
. . . 4
|
| 36 | 19, 35 | eqtr4d 1928 |
. . 3
|
| 37 | 2, 14 | grp2inv 9363 |
. . . . . . . 8
|
| 38 | 37, 21 | eqeqan12d 1901 |
. . . . . . 7
|
| 39 | 38 | anandis 570 |
. . . . . 6
|
| 40 | fveq2 4681 |
. . . . . 6
| |
| 41 | 39, 40 | syl5bi 225 |
. . . . 5
|
| 42 | 41 | ex 402 |
. . . 4
|
| 43 | 42 | r19.21aivv 2183 |
. . 3
|
| 44 | 17, 36, 43 | 3jca 1050 |
. 2
|
| 45 | dff1o6 4853 |
. 2
| |
| 46 | 44, 45 | sylibr 217 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: invfval 9593 grpdlcan 14739 grpdivzer 14740 topgrpbs 14974 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-id 3586 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-grp 9316 df-gid 9317 df-ginv 9318 |