| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. |
| Ref | Expression |
|---|---|
| grpasscan1.1 |
|
| grpasscan1.2 |
|
| Ref | Expression |
|---|---|
| grp2inv |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpasscan1.1 |
. . . . 5
| |
| 2 | grpasscan1.2 |
. . . . 5
| |
| 3 | 1, 2 | grpoinvcl 10373 |
. . . 4
|
| 4 | eqid 2170 |
. . . . 5
| |
| 5 | 1, 4, 2 | grporinv 10376 |
. . . 4
|
| 6 | 3, 5 | syldan 691 |
. . 3
|
| 7 | 1, 4, 2 | grpolinv 10375 |
. . 3
|
| 8 | 6, 7 | eqtr4d 2205 |
. 2
|
| 9 | 1, 2 | grpoinvcl 10373 |
. . . . 5
|
| 10 | 3, 9 | syldan 691 |
. . . 4
|
| 11 | simpr 538 |
. . . 4
| |
| 12 | 10, 11, 3 | 3jca 1328 |
. . 3
|
| 13 | 1 | grpolcan 10380 |
. . 3
|
| 14 | 12, 13 | syldan 691 |
. 2
|
| 15 | 8, 14 | mpbid 256 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: grpinvf 10385 grpdivinv 10389 grpinvdiv 10390 gxneg 10410 gxneg2 10411 gxinv2 10415 gxsuc 10416 gxmul 10422 nvnegneg 10624 ghomf1olem 14621 mult2inv 15787 vec2inv 15818 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1621 ax-gen 1622 ax-8 1623 ax-9 1624 ax-10 1625 ax-11 1626 ax-12 1627 ax-13 1628 ax-14 1629 ax-17 1634 ax-4 1637 ax-5o 1639 ax-6o 1642 ax-9o 1792 ax-10o 1810 ax-16 1883 ax-11o 1893 ax-ext 2152 ax-rep 3628 ax-sep 3638 ax-nul 3645 ax-pow 3681 ax-pr 3719 ax-un 3961 |
| This theorem depends on definitions: df-bi 232 df-or 434 df-an 435 df-3an 1132 df-ex 1645 df-sb 1845 df-eu 2070 df-mo 2071 df-clab 2158 df-cleq 2163 df-clel 2166 df-ne 2297 df-ral 2389 df-rex 2390 df-reu 2391 df-rab 2392 df-v 2571 df-sbc 2731 df-csb 2806 df-dif 2862 df-un 2864 df-in 2866 df-ss 2868 df-nul 3115 df-if 3213 df-pw 3261 df-sn 3274 df-pr 3275 df-op 3278 df-uni 3399 df-br 3540 df-opab 3598 df-id 3779 df-xp 4165 df-rel 4166 df-cnv 4167 df-co 4168 df-dm 4169 df-rn 4170 df-res 4171 df-ima 4172 df-fun 4173 df-fn 4174 df-f 4175 df-f1 4176 df-fo 4177 df-f1o 4178 df-fv 4179 df-opr 5022 df-grpo 10334 df-gid 10335 df-ginv 10336 |