Definition df-minusg

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

	Ref	Expression
Assertion	df-minusg	$$⊢{inv}_g=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼\left(\iota w\in {\mathrm{Base}}_g|w{+}_{g}x=0_g\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cminusg	$$class{inv}_g$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vw	$$setvarw$$
8	7	cv	$$setvarw$$
9		cplusg	$$class{+}_{𝑔}$$
10	5 9	cfv	$$class{+}_g$$
11	3	cv	$$setvarx$$
12	8 11 10	co	$$class\left(w{+}_{g}x\right)$$
13		c0g	$$class{0}_{𝑔}$$
14	5 13	cfv	$$class{0}_g$$
15	12 14	wceq	$$wffw{+}_{g}x=0_g$$
16	15 7 6	crio	$$class\left(\iota w\in {\mathrm{Base}}_g|w{+}_{g}x=0_g\right)$$
17	3 6 16	cmpt	$$class\left(x\in {\mathrm{Base}}_g⟼\left(\iota w\in {\mathrm{Base}}_g|w{+}_{g}x=0_g\right)\right)$$
18	1 2 17	cmpt	$$class\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼\left(\iota w\in {\mathrm{Base}}_g|w{+}_{g}x=0_g\right)\right)\right)$$
19	0 18	wceq	$$wff{inv}_g=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼\left(\iota w\in {\mathrm{Base}}_g|w{+}_{g}x=0_g\right)\right)\right)$$