Definition df-minusg 18955

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 18952	. 2 class invg
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1539	. . . . 5 class 𝑔
6		cbs 17247	. . . . 5 class Base
7	5, 6	cfv 6561	. . . 4 class (Base‘𝑔)
8		vw	. . . . . . . 8 setvar 𝑤
9	8	cv 1539	. . . . . . 7 class 𝑤
10	4	cv 1539	. . . . . . 7 class 𝑥
11		cplusg 17297	. . . . . . . 8 class +g
12	5, 11	cfv 6561	. . . . . . 7 class (+g‘𝑔)
13	9, 10, 12	co 7431	. . . . . 6 class (𝑤(+g‘𝑔)𝑥)
14		c0g 17484	. . . . . . 7 class 0g
15	5, 14	cfv 6561	. . . . . 6 class (0g‘𝑔)
16	13, 15	wceq 1540	. . . . 5 wff (𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)
17	16, 8, 7	crio 7387	. . . 4 class (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))
18	4, 7, 17	cmpt 5225	. . 3 class (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))
19	2, 3, 18	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
20	1, 19	wceq 1540	1 wff invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))

This definition is referenced by:  grpinvfval  18996  grpinvfvalALT  18997