grpidval - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem grpidval 8275

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

**Hypotheses**
Ref	Expression
grpidval.1	⊢ X = ran G
grpidval.2	⊢ U = (Id ‘G)

**Assertion**
Ref	Expression
grpidval	⊢ (G ∈ Grp → U = ∪{u ∈ X∣∀x ∈ X (uGx) = x})

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

**Proof of Theorem grpidval**
Step	Hyp	Ref	Expression
1		fveq2 3835	. . . 4 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → (Id ‘G) = (Id ‘ if(G ∈ Grp, G, {∅, ∅, ∅})))
2		rneq 3426	. . . . . . 7 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → ran G = ran if(G ∈ Grp, G, {∅, ∅, ∅}))
3		rabeq 1855	. . . . . . 7 ⊢ (ran G = ran if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran G∣∀x ∈ ran G(uGx) = x} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran G(uGx) = x})
4	2, 3	syl 10	. . . . . 6 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran G∣∀x ∈ ran G(uGx) = x} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran G(uGx) = x})
5		opreq 4025	. . . . . . . . 9 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → (uGx) = (u if(G ∈ Grp, G, {∅, ∅, ∅})x))
6	5	eqeq1d 1526	. . . . . . . 8 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → ((uGx) = x ↔ (u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x))
7	2, 6	raleq12d 1840	. . . . . . 7 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → (∀x ∈ ran G(uGx) = x ↔ ∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x))
8	7	rabbisdv 1853	. . . . . 6 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran G(uGx) = x} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x})
9	4, 8	eqtrd 1550	. . . . 5 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran G∣∀x ∈ ran G(uGx) = x} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x})
10	9	unieqd 2578	. . . 4 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → ∪{u ∈ ran G∣∀x ∈ ran G(uGx) = x} = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x})
11	1, 10	eqeq12d 1532	. . 3 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → ((Id ‘G) = ∪{u ∈ ran G∣∀x ∈ ran G(uGx) = x} ↔ (Id ‘ if(G ∈ Grp, G, {∅, ∅, ∅})) = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x}))
12		grpidval.2	. . . 4 ⊢ U = (Id ‘G)
13		grpidval.1	. . . . . . 7 ⊢ X = ran G
14		rabeq 1855	. . . . . . 7 ⊢ (X = ran G → {u ∈ X∣∀x ∈ X (uGx) = x} = {u ∈ ran G∣∀x ∈ X (uGx) = x})
15	13, 14	ax-mp 7	. . . . . 6 ⊢ {u ∈ X∣∀x ∈ X (uGx) = x} = {u ∈ ran G∣∀x ∈ X (uGx) = x}
16		raleq1 1832	. . . . . . . . 9 ⊢ (X = ran G → (∀x ∈ X (uGx) = x ↔ ∀x ∈ ran G(uGx) = x))
17	13, 16	ax-mp 7	. . . . . . . 8 ⊢ (∀x ∈ X (uGx) = x ↔ ∀x ∈ ran G(uGx) = x)
18	17	a1i 8	. . . . . . 7 ⊢ (u ∈ ran G → (∀x ∈ X (uGx) = x ↔ ∀x ∈ ran G(uGx) = x))
19	18	rabbii 1851	. . . . . 6 ⊢ {u ∈ ran G∣∀x ∈ X (uGx) = x} = {u ∈ ran G∣∀x ∈ ran G(uGx) = x}
20	15, 19	eqtri 1538	. . . . 5 ⊢ {u ∈ X∣∀x ∈ X (uGx) = x} = {u ∈ ran G∣∀x ∈ ran G(uGx) = x}
21	20	unieqi 2577	. . . 4 ⊢ ∪{u ∈ X∣∀x ∈ X (uGx) = x} = ∪{u ∈ ran G∣∀x ∈ ran G(uGx) = x}
22	12, 21	eqeq12i 1531	. . 3 ⊢ (U = ∪{u ∈ X∣∀x ∈ X (uGx) = x} ↔ (Id ‘G) = ∪{u ∈ ran G∣∀x ∈ ran G(uGx) = x})
23	11, 22	syl5bb 535	. 2 ⊢ (G = if(G ∈ Grp, G, {∅, ∅, ∅}) → (U = ∪{u ∈ X∣∀x ∈ X (uGx) = x} ↔ (Id ‘ if(G ∈ Grp, G, {∅, ∅, ∅})) = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x}))
24		df-gid 8250	. . . 4 ⊢ Id = {g, y∣y = ∪{u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)}}
25	24	fveq1i 3836	. . 3 ⊢ (Id ‘ if(G ∈ Grp, G, {∅, ∅, ∅})) = ({g, y∣y = ∪{u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)}} ‘ if(G ∈ Grp, G, {∅, ∅, ∅}))
26		elisset 1863	. . . . . . . . 9 ⊢ (G ∈ Grp → G ∈ V)
27	26	ancli 294	. . . . . . . 8 ⊢ (G ∈ Grp → (G ∈ Grp ⋀ G ∈ V))
28	27	con3i 98	. . . . . . 7 ⊢ (¬ (G ∈ Grp ⋀ G ∈ V) → ¬ G ∈ Grp)
29		snex 2826	. . . . . . 7 ⊢ {∅, ∅, ∅} ∈ V
30	28, 29	jctir 291	. . . . . 6 ⊢ (¬ (G ∈ Grp ⋀ G ∈ V) → (¬ G ∈ Grp ⋀ {∅, ∅, ∅} ∈ V))
31	30	orri 229	. . . . 5 ⊢ ((G ∈ Grp ⋀ G ∈ V) ⋁ (¬ G ∈ Grp ⋀ {∅, ∅, ∅} ∈ V))
32		ifel 2433	. . . . 5 ⊢ ( if(G ∈ Grp, G, {∅, ∅, ∅}) ∈ V ↔ ((G ∈ Grp ⋀ G ∈ V) ⋁ (¬ G ∈ Grp ⋀ {∅, ∅, ∅} ∈ V)))
33	31, 32	mpbir 188	. . . 4 ⊢ if(G ∈ Grp, G, {∅, ∅, ∅}) ∈ V
34	33	rnex 3448	. . . . . 6 ⊢ ran if(G ∈ Grp, G, {∅, ∅, ∅}) ∈ V
35	34	rabex 2799	. . . . 5 ⊢ {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x} ∈ V
36	35	uniex 3093	. . . 4 ⊢ ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x} ∈ V
37		rneq 3426	. . . . . . . 8 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → ran g = ran if(G ∈ Grp, G, {∅, ∅, ∅}))
38		rabeq 1855	. . . . . . . 8 ⊢ (ran g = ran if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)})
39	37, 38	syl 10	. . . . . . 7 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)})
40		opreq 4025	. . . . . . . . . . 11 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → (ugx) = (u if(G ∈ Grp, G, {∅, ∅, ∅})x))
41	40	eqeq1d 1526	. . . . . . . . . 10 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → ((ugx) = x ↔ (u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x))
42		opreq 4025	. . . . . . . . . . 11 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → (xgu) = (x if(G ∈ Grp, G, {∅, ∅, ∅})u))
43	42	eqeq1d 1526	. . . . . . . . . 10 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → ((xgu) = x ↔ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x))
44	41, 43	anbi12d 631	. . . . . . . . 9 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → (((ugx) = x ⋀ (xgu) = x) ↔ ((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)))
45	37, 44	raleq12d 1840	. . . . . . . 8 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → (∀x ∈ ran g((ugx) = x ⋀ (xgu) = x) ↔ ∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)))
46	45	rabbisdv 1853	. . . . . . 7 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)})
47	39, 46	eqtrd 1550	. . . . . 6 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → {u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)} = {u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)})
48	47	unieqd 2578	. . . . 5 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → ∪{u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)} = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)})
49		0ex 2785	. . . . . . . 8 ⊢ ∅ ∈ V
50	49	grpsn 8273	. . . . . . 7 ⊢ {∅, ∅, ∅} ∈ Grp
51	50	elimel 2451	. . . . . 6 ⊢ if(G ∈ Grp, G, {∅, ∅, ∅}) ∈ Grp
52		eqid 1518	. . . . . . 7 ⊢ ran if(G ∈ Grp, G, {∅, ∅, ∅}) = ran if(G ∈ Grp, G, {∅, ∅, ∅})
53	52	grprlidrid 8270	. . . . . 6 ⊢ ( if(G ∈ Grp, G, {∅, ∅, ∅}) ∈ Grp → ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)} = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x})
54	51, 53	ax-mp 7	. . . . 5 ⊢ ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})((u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x ⋀ (x if(G ∈ Grp, G, {∅, ∅, ∅})u) = x)} = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x}
55	48, 54	syl6eq 1566	. . . 4 ⊢ (g = if(G ∈ Grp, G, {∅, ∅, ∅}) → ∪{u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)} = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x})
56	33, 36, 55	fvopab 3901	. . 3 ⊢ ({g, y∣y = ∪{u ∈ ran g∣∀x ∈ ran g((ugx) = x ⋀ (xgu) = x)}} ‘ if(G ∈ Grp, G, {∅, ∅, ∅})) = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x}
57	25, 56	eqtri 1538	. 2 ⊢ (Id ‘ if(G ∈ Grp, G, {∅, ∅, ∅})) = ∪{u ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})∣∀x ∈ ran if(G ∈ Grp, G, {∅, ∅, ∅})(u if(G ∈ Grp, G, {∅, ∅, ∅})x) = x}
58	23, 57	dedth 2437	1 ⊢ (G ∈ Grp → U = ∪{u ∈ X∣∀x ∈ X (uGx) = x})

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 144 ⋁ wo 220 ⋀ wa 221 = wceq 992 ∈ wcel 994 ∀wral 1691 {crab 1694 Vcvv 1857 ∅c0 2332 ifcif 2415 {csn 2467

cop 2469 ∪cuni 2569 {copab 2740 ran crn 3252 ‘cfv 3263 (class class class)co 4021 Grpcgr 8244 Idcgi 8245

This theorem is referenced by: grpidcl 8276 grpidinv2 8277 cnid 8368 mulid 8373 hilid 9304 zrdivrng 10969

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-op 2474 df-uni 2570 df-br 2693 df-opab 2741 df-id 2913 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-opr 4023 df-grp 8249 df-gid 8250