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 
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A +pQ B ) = <. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = A -> ( 1st ` x ) = ( 1st ` A ) )
2 1 oveq1d 
 |-  ( x = A -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` A ) .N ( 2nd ` y ) ) )
3 fveq2 
 |-  ( x = A -> ( 2nd ` x ) = ( 2nd ` A ) )
4 3 oveq2d 
 |-  ( x = A -> ( ( 1st ` y ) .N ( 2nd ` x ) ) = ( ( 1st ` y ) .N ( 2nd ` A ) ) )
5 2 4 oveq12d 
 |-  ( x = A -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` A ) ) ) )
6 3 oveq1d 
 |-  ( x = A -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` A ) .N ( 2nd ` y ) ) )
7 5 6 opeq12d 
 |-  ( x = A -> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. = <. ( ( ( 1st ` A ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` y ) ) >. )
8 fveq2 
 |-  ( y = B -> ( 2nd ` y ) = ( 2nd ` B ) )
9 8 oveq2d 
 |-  ( y = B -> ( ( 1st ` A ) .N ( 2nd ` y ) ) = ( ( 1st ` A ) .N ( 2nd ` B ) ) )
10 fveq2 
 |-  ( y = B -> ( 1st ` y ) = ( 1st ` B ) )
11 10 oveq1d 
 |-  ( y = B -> ( ( 1st ` y ) .N ( 2nd ` A ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) )
12 9 11 oveq12d 
 |-  ( y = B -> ( ( ( 1st ` A ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
13 8 oveq2d 
 |-  ( y = B -> ( ( 2nd ` A ) .N ( 2nd ` y ) ) = ( ( 2nd ` A ) .N ( 2nd ` B ) ) )
14 12 13 opeq12d 
 |-  ( y = B -> <. ( ( ( 1st ` A ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` y ) ) >. = <. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )
15 df-plpq 
 |-  +pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
16 opex 
 |-  <. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. e. _V
17 7 14 15 16 ovmpo 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A +pQ B ) = <. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )