![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > grpsubval | Structured version Unicode version |
Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
Ref | Expression |
---|---|
grpsubval.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
grpsubval.p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
grpsubval.i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
grpsubval.m |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
grpsubval |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 6206 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fveq2 5798 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | oveq2d 6215 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | grpsubval.b |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | grpsubval.p |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | grpsubval.i |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | grpsubval.m |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 4, 5, 6, 7 | grpsubfval 15698 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | ovex 6224 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | 1, 3, 8, 9 | ovmpt2 6335 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-ral 2803 df-rex 2804 df-reu 2805 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-op 3991 df-uni 4199 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-id 4743 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-1st 6686 df-2nd 6687 df-sbg 15665 |
This theorem is referenced by: grpsubinv 15717 grpsubrcan 15725 grpinvsub 15726 grpinvval2 15727 grpsubid 15728 grpsubid1 15729 grpsubeq0 15730 grpsubadd 15731 grpsubsub 15732 grpaddsubass 15733 grpnpcan 15735 mulgsubdir 15776 pwssub 15786 subgsubcl 15810 subgsub 15811 issubg4 15818 divssub 15859 ghmsub 15873 sylow2blem1 16239 lsmelvalm 16270 ablsub2inv 16420 ablsub4 16422 ablsubsub4 16428 mulgsubdi 16437 eqgabl 16439 gsumsub 16568 gsumsubOLD 16569 dprdfsub 16632 dprdfsubOLD 16639 rngsubdi 16812 rngsubdir 16813 abvsubtri 17042 lmodvsubval2 17122 lmodsubdir 17125 lspsntrim 17301 lidlsubcl 17420 cnfldsub 17968 m2detleiblem7 18564 tgpconcomp 19814 tsmssub 19854 tsmsxplem1 19858 isngp4 20334 ngpsubcan 20336 ngptgp 20353 deg1suble 21711 deg1sub 21712 dchr2sum 22744 ogrpsub 26324 archiabllem2c 26356 grpsubadd0sub 30913 cpscmatgsumbin 31315 lflsub 33035 ldualvsubval 33125 lcdvsubval 35586 baerlem3lem1 35675 baerlem5alem1 35676 baerlem5amN 35684 baerlem5bmN 35685 baerlem5abmN 35686 hdmapsub 35818 |
Copyright terms: Public domain | W3C validator |