Definition df-mpq

Description: Define pre-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, 28-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mpq	$$⊢{\cdot }_{\mathrm{𝑝𝑸}}=\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpq	$$class{\cdot }_{\mathrm{𝑝𝑸}}$$
1		vx	$$setvarx$$
2		cnpi	$$class𝑵$$
3	2 2	cxp	$$class\left(𝑵\times 𝑵\right)$$
4		vy	$$setvary$$
5		c1st	$$class{1}^{st}$$
6	1	cv	$$setvarx$$
7	6 5	cfv	$$class{1}^{st}\left(x\right)$$
8		cmi	$$class{\cdot }_{𝑵}$$
9	4	cv	$$setvary$$
10	9 5	cfv	$$class{1}^{st}\left(y\right)$$
11	7 10 8	co	$$class\left(1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right)\right)$$
12		c2nd	$$class{2}^{nd}$$
13	6 12	cfv	$$class{2}^{nd}\left(x\right)$$
14	9 12	cfv	$$class{2}^{nd}\left(y\right)$$
15	13 14 8	co	$$class\left(2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right)$$
16	11 15	cop	$$class⟨1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩$$
17	1 4 3 3 16	cmpo	$$class\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$
18	0 17	wceq	$$wff{\cdot }_{\mathrm{𝑝𝑸}}=\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$