Definition df-minusg 12712

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 12709	. 2 class invg
2		vg	. . 3 setvar 𝑔
3		cvv 2730	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1347	. . . . 5 class 𝑔
6		cbs 12416	. . . . 5 class Base
7	5, 6	cfv 5198	. . . 4 class (Base‘𝑔)
8		vw	. . . . . . . 8 setvar 𝑤
9	8	cv 1347	. . . . . . 7 class 𝑤
10	4	cv 1347	. . . . . . 7 class 𝑥
11		cplusg 12480	. . . . . . . 8 class +g
12	5, 11	cfv 5198	. . . . . . 7 class (+g‘𝑔)
13	9, 10, 12	co 5853	. . . . . 6 class (𝑤(+g‘𝑔)𝑥)
14		c0g 12596	. . . . . . 7 class 0g
15	5, 14	cfv 5198	. . . . . 6 class (0g‘𝑔)
16	13, 15	wceq 1348	. . . . 5 wff (𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)
17	16, 8, 7	crio 5808	. . . 4 class (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))
18	4, 7, 17	cmpt 4050	. . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))
19	2, 3, 18	cmpt 4050	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
20	1, 19	wceq 1348	1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))

This definition is referenced by:  grpinvfvalg  12745