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 ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A ⋅ 𝑸 B = / 𝑸 ⁡ A ⋅ 𝑝𝑸 B

Proof

Step Hyp Ref Expression
1 df-mq ⊢ ⋅ 𝑸 = / 𝑸 ∘ ⋅ 𝑝𝑸 ↾ 𝑸 × 𝑸
2 1 fveq1i ⊢ ⋅ 𝑸 ⁡ A B = / 𝑸 ∘ ⋅ 𝑝𝑸 ↾ 𝑸 × 𝑸 ⁡ A B
3 2 a1i ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → ⋅ 𝑸 ⁡ A B = / 𝑸 ∘ ⋅ 𝑝𝑸 ↾ 𝑸 × 𝑸 ⁡ A B
4 opelxpi ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A B ∈ 𝑸 × 𝑸
5 4 fvresd ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → / 𝑸 ∘ ⋅ 𝑝𝑸 ↾ 𝑸 × 𝑸 ⁡ A B = / 𝑸 ∘ ⋅ 𝑝𝑸 ⁡ A B
6 df-mpq ⊢ ⋅ 𝑝𝑸 = x ∈ 𝑵 × 𝑵 , y ∈ 𝑵 × 𝑵 ⟼ 1 st ⁡ x ⋅ 𝑵 1 st ⁡ y 2 nd ⁡ x ⋅ 𝑵 2 nd ⁡ y
7 opex ⊢ 1 st ⁡ x ⋅ 𝑵 1 st ⁡ y 2 nd ⁡ x ⋅ 𝑵 2 nd ⁡ y ∈ V
8 6 7 fnmpoi ⊢ ⋅ 𝑝𝑸 Fn 𝑵 × 𝑵 × 𝑵 × 𝑵
9 elpqn ⊢ A ∈ 𝑸 → A ∈ 𝑵 × 𝑵
10 elpqn ⊢ B ∈ 𝑸 → B ∈ 𝑵 × 𝑵
11 opelxpi ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A B ∈ 𝑵 × 𝑵 × 𝑵 × 𝑵
12 9 10 11 syl2an ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A B ∈ 𝑵 × 𝑵 × 𝑵 × 𝑵
13 fvco2 ⊢ ⋅ 𝑝𝑸 Fn 𝑵 × 𝑵 × 𝑵 × 𝑵 ∧ A B ∈ 𝑵 × 𝑵 × 𝑵 × 𝑵 → / 𝑸 ∘ ⋅ 𝑝𝑸 ⁡ A B = / 𝑸 ⁡ ⋅ 𝑝𝑸 ⁡ A B
14 8 12 13 sylancr ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → / 𝑸 ∘ ⋅ 𝑝𝑸 ⁡ A B = / 𝑸 ⁡ ⋅ 𝑝𝑸 ⁡ A B
15 3 5 14 3eqtrd ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → ⋅ 𝑸 ⁡ A B = / 𝑸 ⁡ ⋅ 𝑝𝑸 ⁡ A B
16 df-ov ⊢ A ⋅ 𝑸 B = ⋅ 𝑸 ⁡ A B
17 df-ov ⊢ A ⋅ 𝑝𝑸 B = ⋅ 𝑝𝑸 ⁡ A B
18 17 fveq2i ⊢ / 𝑸 ⁡ A ⋅ 𝑝𝑸 B = / 𝑸 ⁡ ⋅ 𝑝𝑸 ⁡ A B
19 15 16 18 3eqtr4g ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A ⋅ 𝑸 B = / 𝑸 ⁡ A ⋅ 𝑝𝑸 B