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_{𝑝𝑸} = (x \in (𝑵 \times 𝑵), y \in (𝑵 \times 𝑵) ⟼ ⟨1^{st} (x) \cdot_{𝑵} 1^{st} (y), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩)$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-mpq

Detailed syntax breakdown