Theorem grpsubval 18882

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 7360	. 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦)))
2		fveq2 6826	. . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌))
3	2	oveq2d 7369	. 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 18880	. 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))
9		ovex 7386	. 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V
10	1, 3, 8, 9	ovmpo 7513	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  inv_gcminusg 18831  -_gcsg 18832

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932  df-sbg 18835

This theorem is referenced by:  grpsubinv  18909  grpsubrcan  18918  grpinvsub  18919  grpinvval2  18920  grpsubid  18921  grpsubid1  18922  grpsubeq0  18923  grpsubadd0sub  18924  grpsubadd  18925  grpsubsub  18926  grpaddsubass  18927  grpnpcan  18929  pwssub  18951  mulgsubdir  19011  subgsubcl  19034  subgsub  19035  issubg4  19042  qussub  19088  ghmsub  19121  sylow2blem1  19517  lsmelvalm  19548  ablsub2inv  19705  ablsub4  19707  ablsubsub4  19715  mulgsubdi  19726  eqgabl  19731  gsumsub  19845  dprdfsub  19920  ogrpsub  20034  rngsubdi  20074  rngsubdir  20075  abvsubtri  20730  lmodvsubval2  20838  lmodsubdir  20841  lspsntrim  21020  cnfldsub  21322  m2detleiblem7  22530  chpscmatgsumbin  22747  tgpconncomp  24016  tsmssub  24052  tsmsxplem1  24056  isngp4  24516  ngpsubcan  24518  ngptgp  24540  tngngp3  24560  clmpm1dir  25019  cphipval  25159  deg1suble  26028  deg1sub  26029  dchr2sum  27200  symgsubg  33042  cycpmconjv  33097  archiabllem2c  33147  linds2eq  33328  ressply1sub  33515  r1padd1  33549  ply1divalg3  35614  lflsub  39045  ldualvsubval  39135  lcdvsubval  41597  baerlem3lem1  41686  baerlem5alem1  41687  baerlem5amN  41695  baerlem5bmN  41696  baerlem5abmN  41697  hdmapsub  41826  nelsubgsubcld  42471