Metamath Proof Explorer

Theorem mulpqf

Description: Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	mulpqf	$⊢ \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$

Proof

Step	Hyp	Ref	Expression
1		xp1st	$⊢ x \in (𝑵 \times 𝑵) \to 1^{st} (x) \in 𝑵$
2		xp1st	$⊢ y \in (𝑵 \times 𝑵) \to 1^{st} (y) \in 𝑵$
3		mulclpi	$⊢ (1^{st} (x) \in 𝑵 \land 1^{st} (y) \in 𝑵) \to 1^{st} (x) \cdot_{𝑵} 1^{st} (y) \in 𝑵$
4	1 2 3	syl2an	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 1^{st} (x) \cdot_{𝑵} 1^{st} (y) \in 𝑵$
5		xp2nd	$⊢ x \in (𝑵 \times 𝑵) \to 2^{nd} (x) \in 𝑵$
6		xp2nd	$⊢ y \in (𝑵 \times 𝑵) \to 2^{nd} (y) \in 𝑵$
7		mulclpi	$⊢ (2^{nd} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
8	5 6 7	syl2an	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
9	4 8	opelxpd	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to ⟨1^{st} (x) \cdot_{𝑵} 1^{st} (y), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩ \in (𝑵 \times 𝑵)$
10	9	rgen2	$⊢ \forall x \in (𝑵 \times 𝑵) \forall y \in (𝑵 \times 𝑵) ⟨1^{st} (x) \cdot_{𝑵} 1^{st} (y), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩ \in (𝑵 \times 𝑵)$
11		df-mpq	$⊢ \cdot_{𝑝𝑸} = (x \in (𝑵 \times 𝑵), y \in (𝑵 \times 𝑵) ⟼ ⟨1^{st} (x) \cdot_{𝑵} 1^{st} (y), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩)$
12	11	fmpo	$⊢ \forall x \in (𝑵 \times 𝑵) \forall y \in (𝑵 \times 𝑵) ⟨1^{st} (x) \cdot_{𝑵} 1^{st} (y), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩ \in (𝑵 \times 𝑵) \leftrightarrow \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
13	10 12	mpbi	$⊢ \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$