Definition df-rq 3835

Description: Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation.

Assertion

Ref	Expression
df-rq	|- *Q = {<.x, y>. | (x e. Q. /\ (x .Q y) = 1Q)}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-rq

Step	Hyp	Ref	Expression
1		crq 3777	. 2 class *Q
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		cnq 3773	. . . . 5 class Q.
5	3, 4	wcel 1092	. . . 4 wff x e. Q.
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8		cmq 3776	. . . . . 6 class .Q
9	3, 7, 8	co 3001	. . . . 5 class (x .Q y)
10		c1q 3774	. . . . 5 class 1Q
11	9, 10	wceq 1091	. . . 4 wff (x .Q y) = 1Q
12	5, 11	wa 196	. . 3 wff (x e. Q. /\ (x .Q y) = 1Q)
13	12, 2, 6	copab 2055	. 2 class {<.x, y>. | (x e. Q. /\ (x .Q y) = 1Q)}
14	1, 13	wceq 1091	1 wff *Q = {<.x, y>. | (x e. Q. /\ (x .Q y) = 1Q)}

This definition is referenced by:  recmulpq 3864  dmrecpq 3868

metamath.org