# Metamath Proof Explorer

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)↾}_{\left(𝑸\right)}×𝑸$
2 1 fveq1i ${⊢}{+}_{𝑸}\left(⟨{A},{B}⟩\right)=\left({\left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)↾}_{\left(𝑸\right)},×,𝑸\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)↾}_{\left(𝑸\right)},×,𝑸\right)\left(⟨{A},{B}⟩\right)$
4 opelxpi ${⊢}\left({A}\in 𝑸\wedge {B}\in 𝑸\right)\to ⟨{A},{B}⟩\in \left(𝑸×𝑸\right)$
5 4 fvresd ${⊢}\left({A}\in 𝑸\wedge {B}\in 𝑸\right)\to \left({\left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)↾}_{\left(𝑸\right)},×,𝑸\right)\left(⟨{A},{B}⟩\right)=\left({/}_{𝑸}\circ {+}_{\mathrm{𝑝𝑸}}\right)\left(⟨{A},{B}⟩\right)$
6 df-plpq ${⊢}{+}_{\mathrm{𝑝𝑸}}=\left({x}\in \left(𝑵×𝑵\right),{y}\in \left(𝑵×𝑵\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(𝑵×𝑵\right)×\left(𝑵×𝑵\right)\right)$
9 elpqn ${⊢}{A}\in 𝑸\to {A}\in \left(𝑵×𝑵\right)$
10 elpqn ${⊢}{B}\in 𝑸\to {B}\in \left(𝑵×𝑵\right)$
11 opelxpi ${⊢}\left({A}\in \left(𝑵×𝑵\right)\wedge {B}\in \left(𝑵×𝑵\right)\right)\to ⟨{A},{B}⟩\in \left(\left(𝑵×𝑵\right)×\left(𝑵×𝑵\right)\right)$
12 9 10 11 syl2an ${⊢}\left({A}\in 𝑸\wedge {B}\in 𝑸\right)\to ⟨{A},{B}⟩\in \left(\left(𝑵×𝑵\right)×\left(𝑵×𝑵\right)\right)$
13 fvco2 ${⊢}\left({+}_{\mathrm{𝑝𝑸}}Fn\left(\left(𝑵×𝑵\right)×\left(𝑵×𝑵\right)\right)\wedge ⟨{A},{B}⟩\in \left(\left(𝑵×𝑵\right)×\left(𝑵×𝑵\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)$