Theorem addpqnq

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

Proof

Step	Hyp	Ref	Expression
1		df-plq	$$⊢{+}_{𝑸}={\left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)}\times 𝑸$$
2	1	fveq1i	$$⊢{+}_{𝑸}\left(⟨A,B⟩\right)=\left({\left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right)\left(⟨A,B⟩\right)$$
3	2	a1i	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to {+}_{𝑸}\left(⟨A,B⟩\right)=\left({\left({/}_{𝑸}\circ {+}_{\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 {+}_{\mathrm{𝑝𝑸}}\right)\upharpoonright }_{\left(𝑸\right)},\times ,𝑸\right)\left(⟨A,B⟩\right)=\left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)\left(⟨A,B⟩\right)$$
6		df-plpq	$$⊢{+}_{\mathrm{𝑝𝑸}}=\left(x\in \left(𝑵\times 𝑵\right),y\in \left(𝑵\times 𝑵\right)⟼⟨\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\right)$$
7		opex	$$⊢⟨\left(1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)\right),2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩\in \mathrm{V}$$
8	6 7	fnmpoi	$$⊢{+}_{\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({+}_{\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 {+}_{\mathrm{𝑝𝑸}}\right)\left(⟨A,B⟩\right)={/}_{𝑸}\left({+}_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
14	8 12 13	sylancr	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to \left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)\left(⟨A,B⟩\right)={/}_{𝑸}\left({+}_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
15	3 5 14	3eqtrd	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to {+}_{𝑸}\left(⟨A,B⟩\right)={/}_{𝑸}\left({+}_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
16		df-ov	$$⊢A{+}_{𝑸}B={+}_{𝑸}\left(⟨A,B⟩\right)$$
17		df-ov	$$⊢A{+}_{\mathrm{𝑝𝑸}}B={+}_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)$$
18	17	fveq2i	$$⊢{/}_{𝑸}\left(A{+}_{\mathrm{𝑝𝑸}}B\right)={/}_{𝑸}\left({+}_{\mathrm{𝑝𝑸}}\left(⟨A,B⟩\right)\right)$$
19	15 16 18	3eqtr4g	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{+}_{𝑸}B={/}_{𝑸}\left(A{+}_{\mathrm{𝑝𝑸}}B\right)$$