Theorem grpidvallem 9341

Description: The value of the identity element of a group.

Hypotheses

Ref	Expression
grpidval.1	|- X = ran G
grpidval.2	|- U = (Id` G)
grpidvallem.3	|- G e. Grp

Assertion

Ref	Expression
grpidvallem	|- U = U.{u e. X | A.x e. X (uGx) = x}

Distinct variable groups:   x,u,G   u,U,x   u,X,x

Proof of Theorem grpidvallem

Step	Hyp	Ref	Expression
1		grpidval.2	. 2 |- U = (Id` G)
2		grpidvallem.3	. . . 4 |- G e. Grp
3	2	elisseti 2301	. . 3 |- G e. _V
4		grpidval.1	. . . . . 6 |- X = ran G
5	3	rnex 4209	. . . . . 6 |- ran G e. _V
6	4, 5	eqeltri 1967	. . . . 5 |- X e. _V
7	6	rabex 3461	. . . 4 |- {u e. X | A.x e. X (uGx) = x} e. _V
8	7	uniex 3794	. . 3 |- U.{u e. X | A.x e. X (uGx) = x} e. _V
9		rneq 4186	. . . . . . . 8 |- (g = G -> ran g = ran G)
10		rabeq 2289	. . . . . . . 8 |- (ran g = ran G -> {u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)} = {u e. ran G | A.x e. ran g((ugx) = x /\ (xgu) = x)})
11	9, 10	syl 12	. . . . . . 7 |- (g = G -> {u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)} = {u e. ran G | A.x e. ran g((ugx) = x /\ (xgu) = x)})
12	9	adantr 425	. . . . . . . . 9 |- ((g = G /\ u e. ran G) -> ran g = ran G)
13		opreq 4888	. . . . . . . . . . . 12 |- (g = G -> (ugx) = (uGx))
14	13	eqeq1d 1892	. . . . . . . . . . 11 |- (g = G -> ((ugx) = x <-> (uGx) = x))
15	14	adantr 425	. . . . . . . . . 10 |- ((g = G /\ u e. ran G) -> ((ugx) = x <-> (uGx) = x))
16		opreq 4888	. . . . . . . . . . . 12 |- (g = G -> (xgu) = (xGu))
17	16	eqeq1d 1892	. . . . . . . . . . 11 |- (g = G -> ((xgu) = x <-> (xGu) = x))
18	17	adantr 425	. . . . . . . . . 10 |- ((g = G /\ u e. ran G) -> ((xgu) = x <-> (xGu) = x))
19	15, 18	anbi12d 690	. . . . . . . . 9 |- ((g = G /\ u e. ran G) -> (((ugx) = x /\ (xgu) = x) <-> ((uGx) = x /\ (xGu) = x)))
20	12, 19	raleqbidv 2274	. . . . . . . 8 |- ((g = G /\ u e. ran G) -> (A.x e. ran g((ugx) = x /\ (xgu) = x) <-> A.x e. ran G((uGx) = x /\ (xGu) = x)))
21	20	rabbidva 2286	. . . . . . 7 |- (g = G -> {u e. ran G | A.x e. ran g((ugx) = x /\ (xgu) = x)} = {u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)})
22	11, 21	eqtrd 1925	. . . . . 6 |- (g = G -> {u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)} = {u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)})
23	22	unieqd 3188	. . . . 5 |- (g = G -> U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)} = U.{u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)})
24	4	eqcomi 1888	. . . . . . . 8 |- ran G = X
25		rabeq 2289	. . . . . . . 8 |- (ran G = X -> {u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)} = {u e. X | A.x e. ran G((uGx) = x /\ (xGu) = x)})
26	24, 25	ax-mp 7	. . . . . . 7 |- {u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)} = {u e. X | A.x e. ran G((uGx) = x /\ (xGu) = x)}
27	26	unieqi 3187	. . . . . 6 |- U.{u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. ran G((uGx) = x /\ (xGu) = x)}
28		raleq 2266	. . . . . . . . . 10 |- (ran G = X -> (A.x e. ran G((uGx) = x /\ (xGu) = x) <-> A.x e. X ((uGx) = x /\ (xGu) = x)))
29	24, 28	ax-mp 7	. . . . . . . . 9 |- (A.x e. ran G((uGx) = x /\ (xGu) = x) <-> A.x e. X ((uGx) = x /\ (xGu) = x))
30	29	a1i 8	. . . . . . . 8 |- (u e. X -> (A.x e. ran G((uGx) = x /\ (xGu) = x) <-> A.x e. X ((uGx) = x /\ (xGu) = x)))
31	30	rabbiia 2285	. . . . . . 7 |- {u e. X | A.x e. ran G((uGx) = x /\ (xGu) = x)} = {u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)}
32	31	unieqi 3187	. . . . . 6 |- U.{u e. X | A.x e. ran G((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)}
33	4	grprlidrid 9337	. . . . . . 7 |- (G e. Grp -> U.{u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. X (uGx) = x})
34	2, 33	ax-mp 7	. . . . . 6 |- U.{u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. X (uGx) = x}
35	27, 32, 34	3eqtri 1912	. . . . 5 |- U.{u e. ran G | A.x e. ran G((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. X (uGx) = x}
36	23, 35	syl6eq 1944	. . . 4 |- (g = G -> U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)} = U.{u e. X | A.x e. X (uGx) = x})
37		df-gid 9317	. . . . 5 |- Id = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
38		relopab 4104	. . . . . 6 |- Rel {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
39		resid 4258	. . . . . 6 |- (Rel {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}} -> ({<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}} |` _V) = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}})
40	38, 39	ax-mp 7	. . . . 5 |- ({<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}} |` _V) = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
41		resopab 4252	. . . . 5 |- ({<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}} |` _V) = {<.g, y>. | (g e. _V /\ y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)})}
42	37, 40, 41	3eqtr2i 1915	. . . 4 |- Id = {<.g, y>. | (g e. _V /\ y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)})}
43	36, 42	fvopab4g 4742	. . 3 |- ((G e. _V /\ U.{u e. X | A.x e. X (uGx) = x} e. _V) -> (Id` G) = U.{u e. X | A.x e. X (uGx) = x})
44	3, 8, 43	mp2an 761	. 2 |- (Id` G) = U.{u e. X | A.x e. X (uGx) = x}
45	1, 44	eqtri 1908	1 |- U = U.{u e. X | A.x e. X (uGx) = x}

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  {crab 2108  _Vcvv 2292  U.cuni 3177  {copab 3395  ran crn 3987   |` cres 3988  Rel wrel 3991  ` cfv 3998  (class class class)co 4884  Grpcgr 9311  Idcgi 9312

This theorem is referenced by:  idtrgrp 14978

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-opr 4886  df-grp 9316  df-gid 9317

Copyright terms: Public domain