Theorem grpsubval 18959

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 7370	. 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦)))
2		fveq2 6834	. . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌))
3	2	oveq2d 7379	. 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 18957	. 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))
9		ovex 7396	. 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V
10	1, 3, 8, 9	ovmpo 7523	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  inv_gcminusg 18908  -_gcsg 18909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-sbg 18912

This theorem is referenced by:  grpsubinv  18986  grpsubrcan  18995  grpinvsub  18996  grpinvval2  18997  grpsubid  18998  grpsubid1  18999  grpsubeq0  19000  grpsubadd0sub  19001  grpsubadd  19002  grpsubsub  19003  grpaddsubass  19004  grpnpcan  19006  pwssub  19028  mulgsubdir  19088  subgsubcl  19111  subgsub  19112  issubg4  19119  qussub  19164  ghmsub  19197  sylow2blem1  19593  lsmelvalm  19624  ablsub2inv  19781  ablsub4  19783  ablsubsub4  19791  mulgsubdi  19802  eqgabl  19807  gsumsub  19921  dprdfsub  19996  ogrpsub  20110  rngsubdi  20150  rngsubdir  20151  abvsubtri  20806  lmodvsubval2  20914  lmodsubdir  20917  lspsntrim  21095  cnfldsub  21382  m2detleiblem7  22617  chpscmatgsumbin  22834  tgpconncomp  24103  tsmssub  24139  tsmsxplem1  24143  isngp4  24602  ngpsubcan  24604  ngptgp  24626  tngngp3  24646  clmpm1dir  25095  cphipval  25235  deg1suble  26097  deg1sub  26098  dchr2sum  27261  symgsubg  33175  cycpmconjv  33230  archiabllem2c  33283  linds2eq  33471  ressply1sub  33660  r1padd1  33698  ply1divalg3  35877  lflsub  39566  ldualvsubval  39656  lcdvsubval  42117  baerlem3lem1  42206  baerlem5alem1  42207  baerlem5amN  42215  baerlem5bmN  42216  baerlem5abmN  42217  hdmapsub  42346  nelsubgsubcld  42995