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	⊢ ·_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )

Proof

Step	Hyp	Ref	Expression
1		xp1st	⊢ ( 𝑥 ∈ ( N × N ) → ( 1^st ‘ 𝑥 ) ∈ N )
2		xp1st	⊢ ( 𝑦 ∈ ( N × N ) → ( 1^st ‘ 𝑦 ) ∈ N )
3		mulclpi	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ N ∧ ( 1^st ‘ 𝑦 ) ∈ N ) → ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) ∈ N )
4	1 2 3	syl2an	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) ∈ N )
5		xp2nd	⊢ ( 𝑥 ∈ ( N × N ) → ( 2^nd ‘ 𝑥 ) ∈ N )
6		xp2nd	⊢ ( 𝑦 ∈ ( N × N ) → ( 2^nd ‘ 𝑦 ) ∈ N )
7		mulclpi	⊢ ( ( ( 2^nd ‘ 𝑥 ) ∈ N ∧ ( 2^nd ‘ 𝑦 ) ∈ N ) → ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
8	5 6 7	syl2an	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
9	4 8	opelxpd	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ ∈ ( N × N ) )
10	9	rgen2	⊢ ∀ 𝑥 ∈ ( N × N ) ∀ 𝑦 ∈ ( N × N ) ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ ∈ ( N × N )
11		df-mpq	⊢ ·_pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )
12	11	fmpo	⊢ ( ∀ 𝑥 ∈ ( N × N ) ∀ 𝑦 ∈ ( N × N ) ⟨ ( ( 1^st ‘ 𝑥 ) ·_N ( 1^st ‘ 𝑦 ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ ∈ ( N × N ) ↔ ·_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N ) )
13	10 12	mpbi	⊢ ·_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )