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 𝐵 ) = ⟨ ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐵 ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )

Proof

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