Theorem grpsubval 17780

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 6886	. 2 ⊢ (𝑥 = 𝑋 → (𝑥 + (𝐼‘𝑦)) = (𝑋 + (𝐼‘𝑦)))
2		fveq2 6412	. . 3 ⊢ (𝑦 = 𝑌 → (𝐼‘𝑦) = (𝐼‘𝑌))
3	2	oveq2d 6895	. 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 17779	. 2 ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))
9		ovex 6911	. 2 ⊢ (𝑋 + (𝐼‘𝑌)) ∈ V
10	1, 3, 8, 9	ovmpt2 7031	1 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))

Syntax hints:   → wi 4   ∧ wa 385   = wceq 1653   ∈ wcel 2157  ‘cfv 6102  (class class class)co 6879  Basecbs 16183  +_gcplusg 16266  inv_gcminusg 17738  -_gcsg 17739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-rep 4965  ax-sep 4976  ax-nul 4984  ax-pow 5036  ax-pr 5098  ax-un 7184

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ne 2973  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3388  df-sbc 3635  df-csb 3730  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-iun 4713  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5221  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-f1 6107  df-fo 6108  df-f1o 6109  df-fv 6110  df-ov 6882  df-oprab 6883  df-mpt2 6884  df-1st 7402  df-2nd 7403  df-sbg 17742

This theorem is referenced by:  grpsubinv  17803  grpsubrcan  17811  grpinvsub  17812  grpinvval2  17813  grpsubid  17814  grpsubid1  17815  grpsubeq0  17816  grpsubadd0sub  17817  grpsubadd  17818  grpsubsub  17819  grpaddsubass  17820  grpnpcan  17822  pwssub  17844  mulgsubdir  17894  subgsubcl  17917  subgsub  17918  issubg4  17925  qussub  17966  ghmsub  17980  sylow2blem1  18347  lsmelvalm  18378  ablsub2inv  18530  ablsub4  18532  ablsubsub4  18538  mulgsubdi  18549  eqgabl  18554  gsumsub  18662  dprdfsub  18735  ringsubdi  18914  rngsubdir  18915  abvsubtri  19152  lmodvsubval2  19235  lmodsubdir  19238  lspsntrim  19418  cnfldsub  20095  m2detleiblem7  20758  chpscmatgsumbin  20976  tgpconncomp  22243  tsmssub  22279  tsmsxplem1  22283  isngp4  22743  ngpsubcan  22745  ngptgp  22767  tngngp3  22787  clmpm1dir  23229  cphipval  23368  deg1suble  24207  deg1sub  24208  dchr2sum  25349  ogrpsub  30232  archiabllem2c  30264  lflsub  35087  ldualvsubval  35177  lcdvsubval  37638  baerlem3lem1  37727  baerlem5alem1  37728  baerlem5amN  37736  baerlem5bmN  37737  baerlem5abmN  37738  hdmapsub  37867