Definition df-minusg 18107

Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011.)

Assertion

Ref	Expression
df-minusg	⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))

Distinct variable group:   𝑤,𝑔,𝑥

Detailed syntax breakdown of Definition df-minusg

Step	Hyp	Ref	Expression
1		cminusg 18104	. 2 class invg
2		vg	. . 3 setvar 𝑔
3		cvv 3494	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1536	. . . . 5 class 𝑔
6		cbs 16483	. . . . 5 class Base
7	5, 6	cfv 6355	. . . 4 class (Base‘𝑔)
8		vw	. . . . . . . 8 setvar 𝑤
9	8	cv 1536	. . . . . . 7 class 𝑤
10	4	cv 1536	. . . . . . 7 class 𝑥
11		cplusg 16565	. . . . . . . 8 class +g
12	5, 11	cfv 6355	. . . . . . 7 class (+g‘𝑔)
13	9, 10, 12	co 7156	. . . . . 6 class (𝑤(+g‘𝑔)𝑥)
14		c0g 16713	. . . . . . 7 class 0g
15	5, 14	cfv 6355	. . . . . 6 class (0g‘𝑔)
16	13, 15	wceq 1537	. . . . 5 wff (𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)
17	16, 8, 7	crio 7113	. . . 4 class (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))
18	4, 7, 17	cmpt 5146	. . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))
19	2, 3, 18	cmpt 5146	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
20	1, 19	wceq 1537	1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))

This definition is referenced by:  grpinvfval  18142  grpinvfvalALT  18143