![]() |
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 7023 | . 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦))) | |
2 | fveq2 6538 | . . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌)) | |
3 | 2 | oveq2d 7032 | . 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 17904 | . 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) |
9 | ovex 7048 | . 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V | |
10 | 1, 3, 8, 9 | ovmpo 7166 | 1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 +gcplusg 16394 invgcminusg 17862 -gcsg 17863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-1st 7545 df-2nd 7546 df-sbg 17866 |
This theorem is referenced by: grpsubinv 17929 grpsubrcan 17937 grpinvsub 17938 grpinvval2 17939 grpsubid 17940 grpsubid1 17941 grpsubeq0 17942 grpsubadd0sub 17943 grpsubadd 17944 grpsubsub 17945 grpaddsubass 17946 grpnpcan 17948 pwssub 17970 mulgsubdir 18021 subgsubcl 18044 subgsub 18045 issubg4 18052 qussub 18093 ghmsub 18107 sylow2blem1 18475 lsmelvalm 18506 ablsub2inv 18656 ablsub4 18658 ablsubsub4 18664 mulgsubdi 18675 eqgabl 18680 gsumsub 18788 dprdfsub 18860 ringsubdi 19039 rngsubdir 19040 abvsubtri 19296 lmodvsubval2 19379 lmodsubdir 19382 lspsntrim 19560 cnfldsub 20255 m2detleiblem7 20920 chpscmatgsumbin 21136 tgpconncomp 22404 tsmssub 22440 tsmsxplem1 22444 isngp4 22904 ngpsubcan 22906 ngptgp 22928 tngngp3 22948 clmpm1dir 23390 cphipval 23529 deg1suble 24384 deg1sub 24385 dchr2sum 25531 ogrpsub 30377 symgsubg 30390 cycpmconjv 30421 archiabllem2c 30462 linds2eq 30587 lflsub 35734 ldualvsubval 35824 lcdvsubval 38285 baerlem3lem1 38374 baerlem5alem1 38375 baerlem5amN 38383 baerlem5bmN 38384 baerlem5abmN 38385 hdmapsub 38514 nelsubgsubcld 38660 |
Copyright terms: Public domain | W3C validator |