Metamath Proof Explorer


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 𝐵 ) ) )