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	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{\cdot }_{𝑸}B={/}_{𝑸}\left(A{\cdot }_{\mathrm{𝑝𝑸}}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-mq	$$⊢{\cdot }_{𝑸}={\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)}\times 𝑸$$
2	1	fveq1i	$$⊢{\cdot }_{𝑸}\left(⟨A,B⟩\right)=\left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right)\left(⟨A,B⟩\right)$$
3	2	a1i	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to {\cdot }_{𝑸}\left(⟨A,B⟩\right)=\left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right)\left(⟨A,B⟩\right)$$
4		opelxpi	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to ⟨A,B⟩\in \left(𝑸\times 𝑸\right)$$
5	4	fvresd	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to \left({\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right)\left(⟨A,B⟩\right)=\left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\left(⟨A,B⟩\right)$$
6		df-mpq	$$⊢{\cdot }_{\mathrm{𝑝𝑸}}=\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$
7		opex	$$⊢⟨1^{st}\left(x\right){\cdot }_{𝑵}{1}^{st}\left(y\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\in \mathrm{V}$$
8	6 7	fnmpoi	$$⊢{\cdot }_{\mathrm{𝑝𝑸}}Fn\left(\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)\right)$$
9		elpqn	$$⊢A\in 𝑸\to A\in \left(𝑵\times 𝑵\right)$$
10		elpqn	$$⊢B\in 𝑸\to B\in \left(𝑵\times 𝑵\right)$$
11		opelxpi	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to ⟨A,B⟩\in \left(\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)\right)$$
12	9 10 11	syl2an	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to ⟨A,B⟩\in \left(\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)\right)$$
13		fvco2	$$⊢\left({\cdot }_{\mathrm{𝑝𝑸}}Fn\left(\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)\right)\wedge ⟨A,B⟩\in \left(\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)\right)\right)\to \left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\left(⟨A,B⟩\right)={/}_{𝑸}\left({\cdot }_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
14	8 12 13	sylancr	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to \left({/}_{𝑸}\circ {\cdot }_{\mathrm{𝑝𝑸}}\right)\left(⟨A,B⟩\right)={/}_{𝑸}\left({\cdot }_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
15	3 5 14	3eqtrd	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to {\cdot }_{𝑸}\left(⟨A,B⟩\right)={/}_{𝑸}\left({\cdot }_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
16		df-ov	$$⊢A{\cdot }_{𝑸}B={\cdot }_{𝑸}\left(⟨A,B⟩\right)$$
17		df-ov	$$⊢A{\cdot }_{\mathrm{𝑝𝑸}}B={\cdot }_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)$$
18	17	fveq2i	$$⊢{/}_{𝑸}\left(A{\cdot }_{\mathrm{𝑝𝑸}}B\right)={/}_{𝑸}\left({\cdot }_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
19	15 16 18	3eqtr4g	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{\cdot }_{𝑸}B={/}_{𝑸}\left(A{\cdot }_{\mathrm{𝑝𝑸}}B\right)$$