Theorem grpidpropd 18589

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.

Step	Hyp	Ref	Expression
1		grpidpropd.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))
2	1	eqeq1d 2731	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(+g‘𝐾)𝑦) = 𝑦 ↔ (𝑥(+g‘𝐿)𝑦) = 𝑦))
3	1	oveqrspc2v 7414	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧(+g‘𝐾)𝑤) = (𝑧(+g‘𝐿)𝑤))
4	3	oveqrspc2v 7414	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (𝑦(+g‘𝐾)𝑥) = (𝑦(+g‘𝐿)𝑥))
5	4	ancom2s 650	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦(+g‘𝐾)𝑥) = (𝑦(+g‘𝐿)𝑥))
6	5	eqeq1d 2731	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑦(+g‘𝐾)𝑥) = 𝑦 ↔ (𝑦(+g‘𝐿)𝑥) = 𝑦))
7	2, 6	anbi12d 632	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦) ↔ ((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦)))
8	7	anassrs 467	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦) ↔ ((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦)))
9	8	ralbidva 3154	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦) ↔ ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦)))
10	9	pm5.32da 579	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦))))
11		grpidpropd.1	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘𝐾))
12	11	eleq2d 2814	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐾)))
13	11	raleqdv 3299	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦)))
14	12, 13	anbi12d 632	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦))))
15		grpidpropd.2	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘𝐿))
16	15	eleq2d 2814	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐿)))
17	15	raleqdv 3299	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦) ↔ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦)))
18	16, 17	anbi12d 632	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦))))
19	10, 14, 18	3bitr3d 309	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦)) ↔ (𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦))))
20	19	iotabidv 6495	. 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦))) = (℩𝑥(𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦))))
21		eqid 2729	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
22		eqid 2729	. . 3 ⊢ (+g‘𝐾) = (+g‘𝐾)
23		eqid 2729	. . 3 ⊢ (0g‘𝐾) = (0g‘𝐾)
24	21, 22, 23	grpidval 18588	. 2 ⊢ (0g‘𝐾) = (℩𝑥(𝑥 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ (Base‘𝐾)((𝑥(+g‘𝐾)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐾)𝑥) = 𝑦)))
25		eqid 2729	. . 3 ⊢ (Base‘𝐿) = (Base‘𝐿)
26		eqid 2729	. . 3 ⊢ (+g‘𝐿) = (+g‘𝐿)
27		eqid 2729	. . 3 ⊢ (0g‘𝐿) = (0g‘𝐿)
28	25, 26, 27	grpidval 18588	. 2 ⊢ (0g‘𝐿) = (℩𝑥(𝑥 ∈ (Base‘𝐿) ∧ ∀𝑦 ∈ (Base‘𝐿)((𝑥(+g‘𝐿)𝑦) = 𝑦 ∧ (𝑦(+g‘𝐿)𝑥) = 𝑦)))
29	20, 24, 28	3eqtr4g 2789	1 ⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ℩cio 6462  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  0_gc0g 17402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-0g 17404

This theorem is referenced by:  gsumpropd  18605  gsumpropd2lem  18606  mhmpropd  18719  grppropd  18883  grpinvpropd  18947  mulgpropd  19048  prds1  20232  rngidpropd  20324  nzrpropd  20429  drngprop  20653  drngpropd  20678  abvpropd  20744  lbspropd  21006  sralmod0  21095  phlpropd  21564  opsr0  22103  mplbaspropd  22121  ply1mpl0  22141  mat0  22304  nmpropd  24482  nmpropd2  24483  tng0  24531  mdegpropd  25989  ply1divalg2  26044  domnpropd  33227  resv0g  33310  zlm0  33950  hlhils0  41939  hlhil0  41949  mnring0gd  44210