Theorem mulpipq

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

	Ref	Expression
Assertion	mulpipq	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ·pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 ·N 𝐶 ) , ( 𝐵 ·N 𝐷 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		opelxpi	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) )
2		opelxpi	⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) )
3		mulpipq2	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( N × N ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( N × N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ·pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ⟩ )
4	1 2 3	syl2an	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ·pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ⟩ )
5		op1stg	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
6		op1stg	⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
7	5 6	oveqan12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) = ( 𝐴 ·N 𝐶 ) )
8		op2ndg	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
9		op2ndg	⊢ ( ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
10	8 9	oveqan12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) = ( 𝐵 ·N 𝐷 ) )
11	7 10	opeq12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ⟨ ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ·N ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ) ⟩ = ⟨ ( 𝐴 ·N 𝐶 ) , ( 𝐵 ·N 𝐷 ) ⟩ )
12	4 11	eqtrd	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐷 ∈ N ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ·pQ ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 ·N 𝐶 ) , ( 𝐵 ·N 𝐷 ) ⟩ )