This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 +Q 𝐵 ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-plq ⊢ +Q = ( ( [Q] ∘ +pQ ) ↾ ( Q × Q ) )
2 1 fveq1i ⊢ ( +Q ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( [Q] ∘ +pQ ) ↾ ( Q × Q ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
3 2 a1i ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( +Q ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( [Q] ∘ +pQ ) ↾ ( Q × Q ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
4 opelxpi ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( Q × Q ) )
5 4 fvresd ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( ( [Q] ∘ +pQ ) ↾ ( Q × Q ) ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( [Q] ∘ +pQ ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
6 df-plpq ⊢ +pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ )
7 opex ⊢ ⟨ ( ( ( 1st ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) +N ( ( 1st ‘ 𝑦 ) ·N ( 2nd ‘ 𝑥 ) ) ) , ( ( 2nd ‘ 𝑥 ) ·N ( 2nd ‘ 𝑦 ) ) ⟩ ∈ V
8 6 7 fnmpoi ⊢ +pQ Fn ( ( N × N ) × ( N × N ) )
9 elpqn ⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
10 elpqn ⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
11 opelxpi ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( N × N ) × ( N × N ) ) )
12 9 10 11 syl2an ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( N × N ) × ( N × N ) ) )
13 fvco2 ⊢ ( ( +pQ Fn ( ( N × N ) × ( N × N ) ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( N × N ) × ( N × N ) ) ) → ( ( [Q] ∘ +pQ ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( [Q] ‘ ( +pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
14 8 12 13 sylancr ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( [Q] ∘ +pQ ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( [Q] ‘ ( +pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
15 3 5 14 3eqtrd ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( +Q ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( [Q] ‘ ( +pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
16 df-ov ⊢ ( 𝐴 +Q 𝐵 ) = ( +Q ‘ ⟨ 𝐴 , 𝐵 ⟩ )
17 df-ov ⊢ ( 𝐴 +pQ 𝐵 ) = ( +pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ )
18 17 fveq2i ⊢ ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) = ( [Q] ‘ ( +pQ ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
19 15 16 18 3eqtr4g ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 +Q 𝐵 ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) )