Definition df-gdiv 8040

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 8036	. 2 class /g
2		vg	. . . . . 6 set g
3	2	cv 955	. . . . 5 class g
4		cgr 8033	. . . . 5 class Grp
5	3, 4	wcel 958	. . . 4 wff g e. Grp
6		vf	. . . . . 6 set f
7	6	cv 955	. . . . 5 class f
8		vx	. . . . . . . . . 10 set x
9	8	cv 955	. . . . . . . . 9 class x
10	3	crn 3171	. . . . . . . . 9 class ran g
11	9, 10	wcel 958	. . . . . . . 8 wff x e. ran g
12		vy	. . . . . . . . . 10 set y
13	12	cv 955	. . . . . . . . 9 class y
14	13, 10	wcel 958	. . . . . . . 8 wff y e. ran g
15	11, 14	wa 223	. . . . . . 7 wff (x e. ran g /\ y e. ran g)
16		vz	. . . . . . . . 9 set z
17	16	cv 955	. . . . . . . 8 class z
18		cgn 8035	. . . . . . . . . . 11 class inv
19	3, 18	cfv 3182	. . . . . . . . . 10 class (inv` g)
20	13, 19	cfv 3182	. . . . . . . . 9 class ((inv` g)` y)
21	9, 20, 3	co 3963	. . . . . . . 8 class (xg((inv` g)` y))
22	17, 21	wceq 956	. . . . . . 7 wff z = (xg((inv` g)` y))
23	15, 22	wa 223	. . . . . 6 wff ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))
24	23, 8, 12, 16	copab2 3964	. . . . 5 class {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))}
25	7, 24	wceq 956	. . . 4 wff f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))}
26	5, 25	wa 223	. . 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 2666	. 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 956	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 8081  vsfval 8254

Copyright terms: Public domain