Metamath Proof Explorer

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	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +_pQ 𝐵 ) = ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝐴 ) )
2	1	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) )
3		fveq2	⊢ ( 𝑥 = 𝐴 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝐴 ) )
4	3	oveq2d	⊢ ( 𝑥 = 𝐴 → ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝐴 ) ) )
5	2 4	oveq12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
6	3	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) )
7	5 6	opeq12d	⊢ ( 𝑥 = 𝐴 → ⟨ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ = ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )
8		fveq2	⊢ ( 𝑦 = 𝐵 → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ 𝐵 ) )
9	8	oveq2d	⊢ ( 𝑦 = 𝐵 → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) )
10		fveq2	⊢ ( 𝑦 = 𝐵 → ( 1^st ‘ 𝑦 ) = ( 1^st ‘ 𝐵 ) )
11	10	oveq1d	⊢ ( 𝑦 = 𝐵 → ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝐴 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) )
12	9 11	oveq12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
13	8	oveq2d	⊢ ( 𝑦 = 𝐵 → ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) = ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) )
14	12 13	opeq12d	⊢ ( 𝑦 = 𝐵 → ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ = ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )
15		df-plpq	⊢ +_pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )
16		opex	⊢ ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ ∈ V
17	7 14 15 16	ovmpo	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +_pQ 𝐵 ) = ⟨ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) +_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ⟩ )