Definition df-gdiv 9319

Description: Define a function that maps a group operation to the group's division (or subtraction) operation.

Assertion

Ref	Expression
df-gdiv	|- /g = {<.g, f>. | (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))})}

Distinct variable group:   f,g,x,y,z

Detailed syntax breakdown of Definition df-gdiv

Step	Hyp	Ref	Expression
1		cgs 9314	. 2 class /g
2		vg	. . . . . 6 set g
3	2	cv 1297	. . . . 5 class g
4		cgr 9311	. . . . 5 class Grp
5	3, 4	wcel 1300	. . . 4 wff g e. Grp
6		vf	. . . . . 6 set f
7	6	cv 1297	. . . . 5 class f
8		vx	. . . . . . . . . 10 set x
9	8	cv 1297	. . . . . . . . 9 class x
10	3	crn 3987	. . . . . . . . 9 class ran g
11	9, 10	wcel 1300	. . . . . . . 8 wff x e. ran g
12		vy	. . . . . . . . . 10 set y
13	12	cv 1297	. . . . . . . . 9 class y
14	13, 10	wcel 1300	. . . . . . . 8 wff y e. ran g
15	11, 14	wa 240	. . . . . . 7 wff (x e. ran g /\ y e. ran g)
16		vz	. . . . . . . . 9 set z
17	16	cv 1297	. . . . . . . 8 class z
18		cgn 9313	. . . . . . . . . . 11 class inv
19	3, 18	cfv 3998	. . . . . . . . . 10 class (inv` g)
20	13, 19	cfv 3998	. . . . . . . . 9 class ((inv` g)` y)
21	9, 20, 3	co 4884	. . . . . . . 8 class (xg((inv` g)` y))
22	17, 21	wceq 1298	. . . . . . 7 wff z = (xg((inv` g)` y))
23	15, 22	wa 240	. . . . . 6 wff ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))
24	23, 8, 12, 16	copab2 4885	. . . . 5 class {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))}
25	7, 24	wceq 1298	. . . 4 wff f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))}
26	5, 25	wa 240	. . 3 wff (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))})
27	26, 2, 6	copab 3395	. 2 class {<.g, f>. | (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))})}
28	1, 27	wceq 1298	1 wff /g = {<.g, f>. | (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))})}

This definition is referenced by:  grpdivfval 9366  vsfval 9586

Copyright terms: Public domain