Definition df-mq

Description: Define multiplication on positive fractions. 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.4 of Gleason p. 119. (Contributed by NM, 24-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mq	$$⊢{\cdot }_{𝑸}={\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)}\times 𝑸$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmq	$$class{\cdot }_{𝑸}$$
1		cerq	$$class{/}_{𝑸}$$
2		cmpq	$$class{\cdot }_{\mathrm{𝑝𝑸}}$$
3	1 2	ccom	$$class\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)$$
4		cnq	$$class𝑸$$
5	4 4	cxp	$$class\left(𝑸\times 𝑸\right)$$
6	3 5	cres	$$class\left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right)$$
7	0 6	wceq	$$wff{\cdot }_{𝑸}={\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)}\times 𝑸$$