![]() |
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 6772 | . 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦))) | |
2 | fveq2 6304 | . . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌)) | |
3 | 2 | oveq2d 6781 | . 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 17586 | . 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) |
9 | ovex 6793 | . 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V | |
10 | 1, 3, 8, 9 | ovmpt2 6913 | 1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1596 ∈ wcel 2103 ‘cfv 6001 (class class class)co 6765 Basecbs 15980 +gcplusg 16064 invgcminusg 17545 -gcsg 17546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-reu 3021 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-1st 7285 df-2nd 7286 df-sbg 17549 |
This theorem is referenced by: grpsubinv 17610 grpsubrcan 17618 grpinvsub 17619 grpinvval2 17620 grpsubid 17621 grpsubid1 17622 grpsubeq0 17623 grpsubadd0sub 17624 grpsubadd 17625 grpsubsub 17626 grpaddsubass 17627 grpnpcan 17629 pwssub 17651 mulgsubdir 17704 subgsubcl 17727 subgsub 17728 issubg4 17735 qussub 17776 ghmsub 17790 sylow2blem1 18156 lsmelvalm 18187 ablsub2inv 18337 ablsub4 18339 ablsubsub4 18345 mulgsubdi 18356 eqgabl 18361 gsumsub 18469 dprdfsub 18541 ringsubdi 18720 rngsubdir 18721 abvsubtri 18958 lmodvsubval2 19041 lmodsubdir 19044 lspsntrim 19221 cnfldsub 19897 m2detleiblem7 20556 chpscmatgsumbin 20772 tgpconncomp 22038 tsmssub 22074 tsmsxplem1 22078 isngp4 22538 ngpsubcan 22540 ngptgp 22562 tngngp3 22582 clmpm1dir 23024 cphipval 23163 deg1suble 23987 deg1sub 23988 dchr2sum 25118 ogrpsub 29947 archiabllem2c 29979 lflsub 34774 ldualvsubval 34864 lcdvsubval 37326 baerlem3lem1 37415 baerlem5alem1 37416 baerlem5amN 37424 baerlem5bmN 37425 baerlem5abmN 37426 hdmapsub 37558 |
Copyright terms: Public domain | W3C validator |