MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpinvid1 Structured version   Visualization version   GIF version

Theorem grpinvid1 17954
Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
Hypotheses
Ref Expression
grpinv.b 𝐵 = (Base‘𝐺)
grpinv.p + = (+g𝐺)
grpinv.u 0 = (0g𝐺)
grpinv.n 𝑁 = (invg𝐺)
Assertion
Ref Expression
grpinvid1 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑁𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 ))

Proof of Theorem grpinvid1
StepHypRef Expression
1 oveq2 6983 . . . 4 ((𝑁𝑋) = 𝑌 → (𝑋 + (𝑁𝑋)) = (𝑋 + 𝑌))
21adantl 474 . . 3 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑁𝑋) = 𝑌) → (𝑋 + (𝑁𝑋)) = (𝑋 + 𝑌))
3 grpinv.b . . . . . 6 𝐵 = (Base‘𝐺)
4 grpinv.p . . . . . 6 + = (+g𝐺)
5 grpinv.u . . . . . 6 0 = (0g𝐺)
6 grpinv.n . . . . . 6 𝑁 = (invg𝐺)
73, 4, 5, 6grprinv 17953 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 + (𝑁𝑋)) = 0 )
873adant3 1113 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + (𝑁𝑋)) = 0 )
98adantr 473 . . 3 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑁𝑋) = 𝑌) → (𝑋 + (𝑁𝑋)) = 0 )
102, 9eqtr3d 2811 . 2 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑁𝑋) = 𝑌) → (𝑋 + 𝑌) = 0 )
11 oveq2 6983 . . . 4 ((𝑋 + 𝑌) = 0 → ((𝑁𝑋) + (𝑋 + 𝑌)) = ((𝑁𝑋) + 0 ))
1211adantl 474 . . 3 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑋 + 𝑌) = 0 ) → ((𝑁𝑋) + (𝑋 + 𝑌)) = ((𝑁𝑋) + 0 ))
133, 4, 5, 6grplinv 17952 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ((𝑁𝑋) + 𝑋) = 0 )
1413oveq1d 6990 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (((𝑁𝑋) + 𝑋) + 𝑌) = ( 0 + 𝑌))
15143adant3 1113 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (((𝑁𝑋) + 𝑋) + 𝑌) = ( 0 + 𝑌))
163, 6grpinvcl 17951 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
1716adantrr 705 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵)) → (𝑁𝑋) ∈ 𝐵)
18 simprl 759 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵)) → 𝑋𝐵)
19 simprr 761 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵)) → 𝑌𝐵)
2017, 18, 193jca 1109 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵)) → ((𝑁𝑋) ∈ 𝐵𝑋𝐵𝑌𝐵))
213, 4grpass 17913 . . . . . . . 8 ((𝐺 ∈ Grp ∧ ((𝑁𝑋) ∈ 𝐵𝑋𝐵𝑌𝐵)) → (((𝑁𝑋) + 𝑋) + 𝑌) = ((𝑁𝑋) + (𝑋 + 𝑌)))
2220, 21syldan 583 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵)) → (((𝑁𝑋) + 𝑋) + 𝑌) = ((𝑁𝑋) + (𝑋 + 𝑌)))
23223impb 1096 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (((𝑁𝑋) + 𝑋) + 𝑌) = ((𝑁𝑋) + (𝑋 + 𝑌)))
2415, 23eqtr3d 2811 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ( 0 + 𝑌) = ((𝑁𝑋) + (𝑋 + 𝑌)))
253, 4, 5grplid 17934 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝑌𝐵) → ( 0 + 𝑌) = 𝑌)
26253adant2 1112 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ( 0 + 𝑌) = 𝑌)
2724, 26eqtr3d 2811 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑁𝑋) + (𝑋 + 𝑌)) = 𝑌)
2827adantr 473 . . 3 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑋 + 𝑌) = 0 ) → ((𝑁𝑋) + (𝑋 + 𝑌)) = 𝑌)
293, 4, 5grprid 17935 . . . . . 6 ((𝐺 ∈ Grp ∧ (𝑁𝑋) ∈ 𝐵) → ((𝑁𝑋) + 0 ) = (𝑁𝑋))
3016, 29syldan 583 . . . . 5 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ((𝑁𝑋) + 0 ) = (𝑁𝑋))
31303adant3 1113 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑁𝑋) + 0 ) = (𝑁𝑋))
3231adantr 473 . . 3 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑋 + 𝑌) = 0 ) → ((𝑁𝑋) + 0 ) = (𝑁𝑋))
3312, 28, 323eqtr3rd 2818 . 2 (((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) ∧ (𝑋 + 𝑌) = 0 ) → (𝑁𝑋) = 𝑌)
3410, 33impbida 789 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑁𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  cfv 6186  (class class class)co 6975  Basecbs 16338  +gcplusg 16420  0gc0g 16568  Grpcgrp 17904  invgcminusg 17905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-fv 6194  df-riota 6936  df-ov 6978  df-0g 16570  df-mgm 17723  df-sgrp 17765  df-mnd 17776  df-grp 17907  df-minusg 17908
This theorem is referenced by:  grpinvid  17960  grpinvcnv  17967  grpinvadd  17977  subginv  18083  qusinv  18135  ghminv  18149  symginv  18304  frgpinv  18663  cnaddinv  18760  ringnegl  19080  lmodindp1  19521  lmodvsinv2  19544  mhpinvcl  20058  cnfldneg  20289  zringinvg  20352  mdetunilem6  20946  invrvald  21005  dchrinv  25555  baerlem3lem1  38321
  Copyright terms: Public domain W3C validator