This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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} [\{1_{𝑸}\}]$

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 \{1_{𝑸}\}$
5	2 4	cima	$class {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}]$
6	0 5	wceq	$wff *_{𝑸} = {\cdot_{𝑸}}^{-1} [\{1_{𝑸}\}]$