Definition df-rq

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 , 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 NM, 6-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-rq	$$⊢{*}_{𝑸}={{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crq	$$class{*}_{𝑸}$$
1		cmq	$$class{\cdot }_{𝑸}$$
2	1	ccnv	$$class{{\cdot }_{𝑸}}^{-1}$$
3		c1q	$$class{1}_{𝑸}$$
4	3	csn	$$class\left\{1_{𝑸}\right\}$$
5	2 4	cima	$$class{{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]$$
6	0 5	wceq	$$wff{*}_{𝑸}={{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]$$