Definition df-plq

Description: Define addition 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.3 of Gleason p. 117. (Contributed by NM, 24-Aug-1995) (New usage is discouraged.)

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

Detailed syntax breakdown

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