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

Theorem isgrpd 18945
Description: Deduce a group from its properties. Unlike isgrpd2 18943, this one goes straight from the base properties rather than going through Mnd. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
isgrpd.b (𝜑𝐵 = (Base‘𝐺))
isgrpd.p (𝜑+ = (+g𝐺))
isgrpd.c ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
isgrpd.a ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
isgrpd.z (𝜑0𝐵)
isgrpd.i ((𝜑𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
isgrpd.n ((𝜑𝑥𝐵) → 𝑁𝐵)
isgrpd.j ((𝜑𝑥𝐵) → (𝑁 + 𝑥) = 0 )
Assertion
Ref Expression
isgrpd (𝜑𝐺 ∈ Grp)
Distinct variable groups:   𝑥,𝑦,𝑧, +   𝑥, 0 ,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑦,𝑁   𝜑,𝑥,𝑦,𝑧   𝑥,𝐺,𝑦,𝑧
Allowed substitution hints:   𝑁(𝑥,𝑧)

Proof of Theorem isgrpd
StepHypRef Expression
1 isgrpd.b . 2 (𝜑𝐵 = (Base‘𝐺))
2 isgrpd.p . 2 (𝜑+ = (+g𝐺))
3 isgrpd.c . 2 ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
4 isgrpd.a . 2 ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
5 isgrpd.z . 2 (𝜑0𝐵)
6 isgrpd.i . 2 ((𝜑𝑥𝐵) → ( 0 + 𝑥) = 𝑥)
7 isgrpd.n . . 3 ((𝜑𝑥𝐵) → 𝑁𝐵)
8 isgrpd.j . . 3 ((𝜑𝑥𝐵) → (𝑁 + 𝑥) = 0 )
9 oveq1 7420 . . . . 5 (𝑦 = 𝑁 → (𝑦 + 𝑥) = (𝑁 + 𝑥))
109eqeq1d 2728 . . . 4 (𝑦 = 𝑁 → ((𝑦 + 𝑥) = 0 ↔ (𝑁 + 𝑥) = 0 ))
1110rspcev 3607 . . 3 ((𝑁𝐵 ∧ (𝑁 + 𝑥) = 0 ) → ∃𝑦𝐵 (𝑦 + 𝑥) = 0 )
127, 8, 11syl2anc 582 . 2 ((𝜑𝑥𝐵) → ∃𝑦𝐵 (𝑦 + 𝑥) = 0 )
131, 2, 3, 4, 5, 6, 12isgrpde 18944 1 (𝜑𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1534  wcel 2099  wrex 3060  cfv 6543  (class class class)co 7413  Basecbs 17205  +gcplusg 17258  Grpcgrp 18920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5294  ax-nul 5301  ax-pr 5423
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-iota 6495  df-fun 6545  df-fv 6551  df-riota 7369  df-ov 7416  df-0g 17448  df-mgm 18625  df-sgrp 18704  df-mnd 18720  df-grp 18923
This theorem is referenced by:  isgrpi  18946  issubg2  19128  symggrp  19391  isdrngd  20736  isdrngdOLD  20738  psrgrpOLD  21959  cnlmod  25152  dchrabl  27277  motgrp  28464  ldualgrplem  38853  tgrpgrplem  40458  erngdvlem1  40697  erngdvlem1-rN  40705  dvhgrp  40816  mendring  42887
  Copyright terms: Public domain W3C validator