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

Theorem grpidpropd 17433
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 2750 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑥(+g𝐾)𝑦) = 𝑦 ↔ (𝑥(+g𝐿)𝑦) = 𝑦))
31oveqrspc2v 6824 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
43oveqrspc2v 6824 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑥𝐵)) → (𝑦(+g𝐾)𝑥) = (𝑦(+g𝐿)𝑥))
54ancom2s 879 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑦(+g𝐾)𝑥) = (𝑦(+g𝐿)𝑥))
65eqeq1d 2750 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑦(+g𝐾)𝑥) = 𝑦 ↔ (𝑦(+g𝐿)𝑥) = 𝑦))
72, 6anbi12d 749 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
87anassrs 683 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑦𝐵) → (((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
98ralbidva 3111 . . . . 5 ((𝜑𝑥𝐵) → (∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
109pm5.32da 676 . . . 4 (𝜑 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)) ↔ (𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
11 grpidpropd.1 . . . . . 6 (𝜑𝐵 = (Base‘𝐾))
1211eleq2d 2813 . . . . 5 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐾)))
1311raleqdv 3271 . . . . 5 (𝜑 → (∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)))
1412, 13anbi12d 749 . . . 4 (𝜑 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦))))
15 grpidpropd.2 . . . . . 6 (𝜑𝐵 = (Base‘𝐿))
1615eleq2d 2813 . . . . 5 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐿)))
1715raleqdv 3271 . . . . 5 (𝜑 → (∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
1816, 17anbi12d 749 . . . 4 (𝜑 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
1910, 14, 183bitr3d 298 . . 3 (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
2019iotabidv 6021 . 2 (𝜑 → (℩𝑥(𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦))) = (℩𝑥(𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦))))
21 eqid 2748 . . 3 (Base‘𝐾) = (Base‘𝐾)
22 eqid 2748 . . 3 (+g𝐾) = (+g𝐾)
23 eqid 2748 . . 3 (0g𝐾) = (0g𝐾)
2421, 22, 23grpidval 17432 . 2 (0g𝐾) = (℩𝑥(𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g𝐾)𝑦) = 𝑦 ∧ (𝑦(+g𝐾)𝑥) = 𝑦)))
25 eqid 2748 . . 3 (Base‘𝐿) = (Base‘𝐿)
26 eqid 2748 . . 3 (+g𝐿) = (+g𝐿)
27 eqid 2748 . . 3 (0g𝐿) = (0g𝐿)
2825, 26, 27grpidval 17432 . 2 (0g𝐿) = (℩𝑥(𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g𝐿)𝑦) = 𝑦 ∧ (𝑦(+g𝐿)𝑥) = 𝑦)))
2920, 24, 283eqtr4g 2807 1 (𝜑 → (0g𝐾) = (0g𝐿))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1620  wcel 2127  wral 3038  cio 5998  cfv 6037  (class class class)co 6801  Basecbs 16030  +gcplusg 16114  0gc0g 16273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-iota 6000  df-fun 6039  df-fv 6045  df-ov 6804  df-0g 16275
This theorem is referenced by:  gsumpropd  17444  gsumpropd2lem  17445  mhmpropd  17513  grppropd  17609  grpinvpropd  17662  mulgpropd  17756  prds1  18785  rngidpropd  18866  drngprop  18931  drngpropd  18947  abvpropd  19015  lbspropd  19272  sralmod0  19361  opsr0  19761  mplbaspropd  19780  ply1mpl0  19798  phlpropd  20173  mat0  20396  nmpropd  22570  nmpropd2  22571  tng0  22619  mdegpropd  24014  ply1divalg2  24068  resv0g  30116  zlm0  30286  hlhils0  37708  hlhil0  37718
  Copyright terms: Public domain W3C validator