![]() |
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 7361 | . 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦))) | |
2 | fveq2 6840 | . . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌)) | |
3 | 2 | oveq2d 7370 | . 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 18791 | . 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))) |
9 | ovex 7387 | . 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V | |
10 | 1, 3, 8, 9 | ovmpo 7512 | 1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ‘cfv 6494 (class class class)co 7354 Basecbs 17080 +gcplusg 17130 invgcminusg 18746 -gcsg 18747 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-fv 6502 df-ov 7357 df-oprab 7358 df-mpo 7359 df-1st 7918 df-2nd 7919 df-sbg 18750 |
This theorem is referenced by: grpsubinv 18816 grpsubrcan 18824 grpinvsub 18825 grpinvval2 18826 grpsubid 18827 grpsubid1 18828 grpsubeq0 18829 grpsubadd0sub 18830 grpsubadd 18831 grpsubsub 18832 grpaddsubass 18833 grpnpcan 18835 pwssub 18857 mulgsubdir 18912 subgsubcl 18935 subgsub 18936 issubg4 18943 qussub 18986 ghmsub 19012 sylow2blem1 19398 lsmelvalm 19429 ablsub2inv 19585 ablsub4 19587 ablsubsub4 19593 mulgsubdi 19604 eqgabl 19609 gsumsub 19721 dprdfsub 19796 ringsubdi 20019 ringsubdir 20020 abvsubtri 20290 lmodvsubval2 20373 lmodsubdir 20376 lspsntrim 20555 cnfldsub 20821 m2detleiblem7 21972 chpscmatgsumbin 22189 tgpconncomp 23460 tsmssub 23496 tsmsxplem1 23500 isngp4 23964 ngpsubcan 23966 ngptgp 23988 tngngp3 24016 clmpm1dir 24462 cphipval 24603 deg1suble 25468 deg1sub 25469 dchr2sum 26617 ogrpsub 31819 symgsubg 31833 cycpmconjv 31886 archiabllem2c 31926 linds2eq 32063 ressply1sub 32171 lflsub 37518 ldualvsubval 37608 lcdvsubval 40070 baerlem3lem1 40159 baerlem5alem1 40160 baerlem5amN 40168 baerlem5bmN 40169 baerlem5abmN 40170 hdmapsub 40299 nelsubgsubcld 40661 |
Copyright terms: Public domain | W3C validator |