Theorem mulpqnq

Description: Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995) (Revised by Mario Carneiro, 26-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	mulpqnq	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-mq	⊢ ·Q = ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) )
2	1	fveq1i	⊢ ( ·Q ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
3	2	a1i	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ·Q ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
4		opelxpi	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( Q × Q ) )
5	4	fvresd	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( ( [Q] ∘ ·pQ ) ↾ ( Q × Q ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( [Q] ∘ ·pQ ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
6		df-mpq	⊢ ·pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ )
7		opex	⊢ ⟨ ( ( 1st ‘ 𝑥 ) ·N ( 1st ‘ 𝑦 ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ ∈ V
8	6 7	fnmpoi	⊢ ·pQ Fn ( ( N × N ) × ( N × N ) )
9		elpqn	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
10		elpqn	⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
11		opelxpi	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( N × N ) × ( N × N ) ) )
12	9 10 11	syl2an	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( N × N ) × ( N × N ) ) )
13		fvco2	⊢ ( ( ·pQ Fn ( ( N × N ) × ( N × N ) ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( N × N ) × ( N × N ) ) ) → ( ( [Q] ∘ ·pQ ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( [Q] ‘ ( ·pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
14	8 12 13	sylancr	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( [Q] ∘ ·pQ ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( [Q] ‘ ( ·pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
15	3 5 14	3eqtrd	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ·Q ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( [Q] ‘ ( ·pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
16		df-ov	⊢ ( 𝐴 ·Q 𝐵 ) = ( ·Q ‘ ⟨ 𝐴 , 𝐵 ⟩ )
17		df-ov	⊢ ( 𝐴 ·pQ 𝐵 ) = ( ·pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ )
18	17	fveq2i	⊢ ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) = ( [Q] ‘ ( ·pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
19	15 16 18	3eqtr4g	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) )