Definition df-rq 7314

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, 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. (Contributed by Jim Kingdon, 20-Sep-2019.)

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-rq

Step	Hyp	Ref	Expression
1		crq 7246	. 2 class *Q
2		vx	. . . . . 6 setvar x
3	2	cv 1347	. . . . 5 class x
4		cnq 7242	. . . . 5 class Q.
5	3, 4	wcel 2141	. . . 4 wff x e. Q.
6		vy	. . . . . 6 setvar y
7	6	cv 1347	. . . . 5 class y
8	7, 4	wcel 2141	. . . 4 wff y e. Q.
9		cmq 7245	. . . . . 6 class .Q
10	3, 7, 9	co 5853	. . . . 5 class ( x .Q y )
11		c1q 7243	. . . . 5 class 1Q
12	10, 11	wceq 1348	. . . 4 wff ( x .Q y ) = 1Q
13	5, 8, 12	w3a 973	. . 3 wff ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q )
14	13, 2, 6	copab 4049	. 2 class { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
15	1, 14	wceq 1348	1 wff *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }

This definition is referenced by:  recmulnqg  7353