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 
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( /Q ` ( A +pQ B ) ) )

Proof

Step Hyp Ref Expression
1 df-plq 
 |-  +Q = ( ( /Q o. +pQ ) |` ( Q. X. Q. ) )
2 1 fveq1i 
 |-  ( +Q ` <. A , B >. ) = ( ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. )
3 2 a1i 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( +Q ` <. A , B >. ) = ( ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) )
4 opelxpi 
 |-  ( ( A e. Q. /\ B e. Q. ) -> <. A , B >. e. ( Q. X. Q. ) )
5 4 fvresd 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) ` <. A , B >. ) = ( ( /Q o. +pQ ) ` <. A , B >. ) )
6 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 ) ) >. )
7 opex 
 |-  <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. _V
8 6 7 fnmpoi 
 |-  +pQ Fn ( ( N. X. N. ) X. ( N. X. N. ) )
9 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
10 elpqn 
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
11 opelxpi 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) )
12 9 10 11 syl2an 
 |-  ( ( A e. Q. /\ B e. Q. ) -> <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) )
13 fvco2 
 |-  ( ( +pQ Fn ( ( N. X. N. ) X. ( N. X. N. ) ) /\ <. A , B >. e. ( ( N. X. N. ) X. ( N. X. N. ) ) ) -> ( ( /Q o. +pQ ) ` <. A , B >. ) = ( /Q ` ( +pQ ` <. A , B >. ) ) )
14 8 12 13 sylancr 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( ( /Q o. +pQ ) ` <. A , B >. ) = ( /Q ` ( +pQ ` <. A , B >. ) ) )
15 3 5 14 3eqtrd 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( +Q ` <. A , B >. ) = ( /Q ` ( +pQ ` <. A , B >. ) ) )
16 df-ov 
 |-  ( A +Q B ) = ( +Q ` <. A , B >. )
17 df-ov 
 |-  ( A +pQ B ) = ( +pQ ` <. A , B >. )
18 17 fveq2i 
 |-  ( /Q ` ( A +pQ B ) ) = ( /Q ` ( +pQ ` <. A , B >. ) )
19 15 16 18 3eqtr4g 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( /Q ` ( A +pQ B ) ) )