Theorem grpsubval 18904

Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)

Hypotheses

Ref	Expression
grpsubval.b	⊢ 𝐵 = (Base‘𝐺)
grpsubval.p	⊢ + = (+g‘𝐺)
grpsubval.i	⊢ 𝐼 = (invg‘𝐺)
grpsubval.m	⊢ − = (-g‘𝐺)

Assertion

Ref	Expression
grpsubval	⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))

Proof of Theorem grpsubval

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7359	. 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦)))
2		fveq2 6828	. . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌))
3	2	oveq2d 7368	. 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 18902	. 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))
9		ovex 7385	. 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V
10	1, 3, 8, 9	ovmpo 7512	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ‘cfv 6487  (class class class)co 7352  Basecbs 17126  +_gcplusg 17167  inv_gcminusg 18853  -_gcsg 18854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-sbg 18857

This theorem is referenced by:  grpsubinv  18931  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  19033  subgsubcl  19056  subgsub  19057  issubg4  19064  qussub  19109  ghmsub  19142  sylow2blem1  19538  lsmelvalm  19569  ablsub2inv  19726  ablsub4  19728  ablsubsub4  19736  mulgsubdi  19747  eqgabl  19752  gsumsub  19866  dprdfsub  19941  ogrpsub  20055  rngsubdi  20095  rngsubdir  20096  abvsubtri  20748  lmodvsubval2  20856  lmodsubdir  20859  lspsntrim  21038  cnfldsub  21340  m2detleiblem7  22548  chpscmatgsumbin  22765  tgpconncomp  24034  tsmssub  24070  tsmsxplem1  24074  isngp4  24533  ngpsubcan  24535  ngptgp  24557  tngngp3  24577  clmpm1dir  25036  cphipval  25176  deg1suble  26045  deg1sub  26046  dchr2sum  27217  symgsubg  33063  cycpmconjv  33118  archiabllem2c  33171  linds2eq  33353  ressply1sub  33540  r1padd1  33575  ply1divalg3  35693  lflsub  39172  ldualvsubval  39262  lcdvsubval  41723  baerlem3lem1  41812  baerlem5alem1  41813  baerlem5amN  41821  baerlem5bmN  41822  baerlem5abmN  41823  hdmapsub  41952  nelsubgsubcld  42597