Theorem addpipq2

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

	Ref	Expression
Assertion	addpipq2	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to A{+}_{\mathrm{𝑝𝑸}}B=⟨\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){+}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=A\to 1^{st}\left(x\right)=1^{st}\left(A\right)$$
2	1	oveq1d	$$⊢x=A\to 1^{st}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)=1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)$$
3		fveq2	$$⊢x=A\to 2^{nd}\left(x\right)=2^{nd}\left(A\right)$$
4	3	oveq2d	$$⊢x=A\to 1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(x\right)=1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)$$
5	2 4	oveq12d	$$⊢x=A\to \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)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
6	3	oveq1d	$$⊢x=A\to 2^{nd}\left(x\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)=2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)$$
7	5 6	opeq12d	$$⊢x=A\to ⟨\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)⟩=⟨\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩$$
8		fveq2	$$⊢y=B\to 2^{nd}\left(y\right)=2^{nd}\left(B\right)$$
9	8	oveq2d	$$⊢y=B\to 1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)=1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)$$
10		fveq2	$$⊢y=B\to 1^{st}\left(y\right)=1^{st}\left(B\right)$$
11	10	oveq1d	$$⊢y=B\to 1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)=1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)$$
12	9 11	oveq12d	$$⊢y=B\to \left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)=\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){+}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right)$$
13	8	oveq2d	$$⊢y=B\to 2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)=2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)$$
14	12 13	opeq12d	$$⊢y=B\to ⟨\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)\right){+}_{𝑵}\left(1^{st}\left(y\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(y\right)⟩=⟨\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){+}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)⟩$$
15		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)$$
16		opex	$$⊢⟨\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){+}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)⟩\in \mathrm{V}$$
17	7 14 15 16	ovmpo	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to A{+}_{\mathrm{𝑝𝑸}}B=⟨\left(1^{st}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)\right){+}_{𝑵}\left(1^{st}\left(B\right){\cdot }_{𝑵}{2}^{nd}\left(A\right)\right),2^{nd}\left(A\right){\cdot }_{𝑵}{2}^{nd}\left(B\right)⟩$$