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 𝐵 ) ) )