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

Theorem grpidpropd 17931
 Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.)
Hypotheses
Ref Expression
grpidpropd.1 (𝜑𝐵 = (Base‘𝐾))
grpidpropd.2 (𝜑𝐵 = (Base‘𝐿))
grpidpropd.3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
Assertion
Ref Expression
grpidpropd (𝜑 → (0g𝐾) = (0g𝐿))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦   𝜑,𝑥,𝑦   𝑥,𝐿,𝑦

Proof of Theorem grpidpropd
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grpidpropd.3 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
21eqeq1d 2761 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑥(+g𝐾)𝑦) = 𝑦 ↔ (𝑥(+g𝐿)𝑦) = 𝑦))
31oveqrspc2v 7178 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
43oveqrspc2v 7178 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑥𝐵)) → (𝑦(+g𝐾)𝑥) = (𝑦(+g𝐿)𝑥))
54ancom2s 650 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦(+g𝐾)𝑥) = (𝑦(+g𝐿)𝑥))
65eqeq1d 2761 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑦(+g𝐾)𝑥) = 𝑦 ↔ (𝑦(+g𝐿)𝑥) = 𝑦))
72, 6anbi12d 634 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
87anassrs 472 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
98ralbidva 3126 . . . . 5 ((𝜑𝑥𝐵) → (∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
109pm5.32da 583 . . . 4 (𝜑 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)) ↔ (𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
11 grpidpropd.1 . . . . . 6 (𝜑𝐵 = (Base‘𝐾))
1211eleq2d 2838 . . . . 5 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐾)))
1311raleqdv 3330 . . . . 5 (𝜑 → (∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)))
1412, 13anbi12d 634 . . . 4 (𝜑 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦))))
15 grpidpropd.2 . . . . . 6 (𝜑𝐵 = (Base‘𝐿))
1615eleq2d 2838 . . . . 5 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐿)))
1715raleqdv 3330 . . . . 5 (𝜑 → (∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
1816, 17anbi12d 634 . . . 4 (𝜑 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
1910, 14, 183bitr3d 313 . . 3 (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
2019iotabidv 6320 . 2 (𝜑 → (℩𝑥(𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦))) = (℩𝑥(𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
21 eqid 2759 . . 3 (Base‘𝐾) = (Base‘𝐾)
22 eqid 2759 . . 3 (+g𝐾) = (+g𝐾)
23 eqid 2759 . . 3 (0g𝐾) = (0g𝐾)
2421, 22, 23grpidval 17930 . 2 (0g𝐾) = (℩𝑥(𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)))
25 eqid 2759 . . 3 (Base‘𝐿) = (Base‘𝐿)
26 eqid 2759 . . 3 (+g𝐿) = (+g𝐿)
27 eqid 2759 . . 3 (0g𝐿) = (0g𝐿)
2825, 26, 27grpidval 17930 . 2 (0g𝐿) = (℩𝑥(𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
2920, 24, 283eqtr4g 2819 1 (𝜑 → (0g𝐾) = (0g𝐿))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ℩cio 6293  ‘cfv 6336  (class class class)co 7151  Basecbs 16534  +gcplusg 16616  0gc0g 16764 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7154  df-0g 16766 This theorem is referenced by:  gsumpropd  17947  gsumpropd2lem  17948  mhmpropd  18021  grppropd  18178  grpinvpropd  18234  mulgpropd  18329  prds1  19428  rngidpropd  19509  drngprop  19574  drngpropd  19590  abvpropd  19674  lbspropd  19932  sralmod0  20021  phlpropd  20413  opsr0  20935  mplbaspropd  20954  ply1mpl0  20972  mat0  21110  nmpropd  23289  nmpropd2  23290  tng0  23338  mdegpropd  24777  ply1divalg2  24831  resv0g  31054  zlm0  31424  hlhils0  39514  hlhil0  39524  mnring0gd  41295
 Copyright terms: Public domain W3C validator