Metamath Proof Explorer


Theorem mulpipq2

Description: Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulpipq2 ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐵 ) = ⟨ ( ( 1st𝐴 ) ·N ( 1st𝐵 ) ) , ( ( 2nd𝐴 ) ·N ( 2nd𝐵 ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑥 = 𝐴 → ( 1st𝑥 ) = ( 1st𝐴 ) )
2 1 oveq1d ( 𝑥 = 𝐴 → ( ( 1st𝑥 ) ·N ( 1st𝑦 ) ) = ( ( 1st𝐴 ) ·N ( 1st𝑦 ) ) )
3 fveq2 ( 𝑥 = 𝐴 → ( 2nd𝑥 ) = ( 2nd𝐴 ) )
4 3 oveq1d ( 𝑥 = 𝐴 → ( ( 2nd𝑥 ) ·N ( 2nd𝑦 ) ) = ( ( 2nd𝐴 ) ·N ( 2nd𝑦 ) ) )
5 2 4 opeq12d ( 𝑥 = 𝐴 → ⟨ ( ( 1st𝑥 ) ·N ( 1st𝑦 ) ) , ( ( 2nd𝑥 ) ·N ( 2nd𝑦 ) ) ⟩ = ⟨ ( ( 1st𝐴 ) ·N ( 1st𝑦 ) ) , ( ( 2nd𝐴 ) ·N ( 2nd𝑦 ) ) ⟩ )
6 fveq2 ( 𝑦 = 𝐵 → ( 1st𝑦 ) = ( 1st𝐵 ) )
7 6 oveq2d ( 𝑦 = 𝐵 → ( ( 1st𝐴 ) ·N ( 1st𝑦 ) ) = ( ( 1st𝐴 ) ·N ( 1st𝐵 ) ) )
8 fveq2 ( 𝑦 = 𝐵 → ( 2nd𝑦 ) = ( 2nd𝐵 ) )
9 8 oveq2d ( 𝑦 = 𝐵 → ( ( 2nd𝐴 ) ·N ( 2nd𝑦 ) ) = ( ( 2nd𝐴 ) ·N ( 2nd𝐵 ) ) )
10 7 9 opeq12d ( 𝑦 = 𝐵 → ⟨ ( ( 1st𝐴 ) ·N ( 1st𝑦 ) ) , ( ( 2nd𝐴 ) ·N ( 2nd𝑦 ) ) ⟩ = ⟨ ( ( 1st𝐴 ) ·N ( 1st𝐵 ) ) , ( ( 2nd𝐴 ) ·N ( 2nd𝐵 ) ) ⟩ )
11 df-mpq ·pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( 1st𝑥 ) ·N ( 1st𝑦 ) ) , ( ( 2nd𝑥 ) ·N ( 2nd𝑦 ) ) ⟩ )
12 opex ⟨ ( ( 1st𝐴 ) ·N ( 1st𝐵 ) ) , ( ( 2nd𝐴 ) ·N ( 2nd𝐵 ) ) ⟩ ∈ V
13 5 10 11 12 ovmpo ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐵 ) = ⟨ ( ( 1st𝐴 ) ·N ( 1st𝐵 ) ) , ( ( 2nd𝐴 ) ·N ( 2nd𝐵 ) ) ⟩ )