![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > grpsubval | Structured version Visualization version GIF version |
Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
Ref | Expression |
---|---|
grpsubval.b | ⊢ 𝐵 = (Base‘𝐺) |
grpsubval.p | ⊢ + = (+g‘𝐺) |
grpsubval.i | ⊢ 𝐼 = (invg‘𝐺) |
grpsubval.m | ⊢ − = (-g‘𝐺) |
Ref | Expression |
---|---|
grpsubval | ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 7418 | . 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦))) | |
2 | fveq2 6890 | . . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌)) | |
3 | 2 | oveq2d 7427 | . 2 ⊢ (𝑦 = 𝑌 → (𝑋 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑌))) |
4 | grpsubval.b | . . 3 ⊢ 𝐵 = (Base‘𝐺) | |
5 | grpsubval.p | . . 3 ⊢ + = (+g‘𝐺) | |
6 | grpsubval.i | . . 3 ⊢ 𝐼 = (invg‘𝐺) | |
7 | grpsubval.m | . . 3 ⊢ − = (-g‘𝐺) | |
8 | 4, 5, 6, 7 | grpsubfval 18904 | . 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) |
9 | ovex 7444 | . 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V | |
10 | 1, 3, 8, 9 | ovmpo 7570 | 1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ‘cfv 6542 (class class class)co 7411 Basecbs 17148 +gcplusg 17201 invgcminusg 18856 -gcsg 18857 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-sbg 18860 |
This theorem is referenced by: grpsubinv 18932 grpsubrcan 18940 grpinvsub 18941 grpinvval2 18942 grpsubid 18943 grpsubid1 18944 grpsubeq0 18945 grpsubadd0sub 18946 grpsubadd 18947 grpsubsub 18948 grpaddsubass 18949 grpnpcan 18951 pwssub 18973 mulgsubdir 19030 subgsubcl 19053 subgsub 19054 issubg4 19061 qussub 19106 ghmsub 19138 sylow2blem1 19529 lsmelvalm 19560 ablsub2inv 19717 ablsub4 19719 ablsubsub4 19727 mulgsubdi 19738 eqgabl 19743 gsumsub 19857 dprdfsub 19932 rngsubdi 20065 rngsubdir 20066 abvsubtri 20586 lmodvsubval2 20671 lmodsubdir 20674 lspsntrim 20853 cnfldsub 21173 m2detleiblem7 22349 chpscmatgsumbin 22566 tgpconncomp 23837 tsmssub 23873 tsmsxplem1 23877 isngp4 24341 ngpsubcan 24343 ngptgp 24365 tngngp3 24393 clmpm1dir 24850 cphipval 24991 deg1suble 25860 deg1sub 25861 dchr2sum 27012 ogrpsub 32504 symgsubg 32518 cycpmconjv 32571 archiabllem2c 32611 linds2eq 32771 ressply1sub 32933 r1padd1 32953 lflsub 38240 ldualvsubval 38330 lcdvsubval 40792 baerlem3lem1 40881 baerlem5alem1 40882 baerlem5amN 40890 baerlem5bmN 40891 baerlem5abmN 40892 hdmapsub 41021 nelsubgsubcld 41378 |
Copyright terms: Public domain | W3C validator |