Metamath Proof Explorer

Theorem addpipq

Description: Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion addpipq 
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. +pQ <. C , D >. ) = <. ( ( A .N D ) +N ( C .N B ) ) , ( B .N D ) >. )

Proof

Step Hyp Ref Expression
1 opelxpi 
 |-  ( ( A e. N. /\ B e. N. ) -> <. A , B >. e. ( N. X. N. ) )
2 opelxpi 
 |-  ( ( C e. N. /\ D e. N. ) -> <. C , D >. e. ( N. X. N. ) )
3 addpipq2 
 |-  ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) -> ( <. A , B >. +pQ <. C , D >. ) = <. ( ( ( 1st ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) +N ( ( 1st ` <. C , D >. ) .N ( 2nd ` <. A , B >. ) ) ) , ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) >. )
4 1 2 3 syl2an 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. +pQ <. C , D >. ) = <. ( ( ( 1st ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) +N ( ( 1st ` <. C , D >. ) .N ( 2nd ` <. A , B >. ) ) ) , ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) >. )
5 op1stg 
 |-  ( ( A e. N. /\ B e. N. ) -> ( 1st ` <. A , B >. ) = A )
6 op2ndg 
 |-  ( ( C e. N. /\ D e. N. ) -> ( 2nd ` <. C , D >. ) = D )
7 5 6 oveqan12d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( ( 1st ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) = ( A .N D ) )
8 op1stg 
 |-  ( ( C e. N. /\ D e. N. ) -> ( 1st ` <. C , D >. ) = C )
9 op2ndg 
 |-  ( ( A e. N. /\ B e. N. ) -> ( 2nd ` <. A , B >. ) = B )
10 8 9 oveqan12rd 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( ( 1st ` <. C , D >. ) .N ( 2nd ` <. A , B >. ) ) = ( C .N B ) )
11 7 10 oveq12d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( ( ( 1st ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) +N ( ( 1st ` <. C , D >. ) .N ( 2nd ` <. A , B >. ) ) ) = ( ( A .N D ) +N ( C .N B ) ) )
12 9 6 oveqan12d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) = ( B .N D ) )
13 11 12 opeq12d 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> <. ( ( ( 1st ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) +N ( ( 1st ` <. C , D >. ) .N ( 2nd ` <. A , B >. ) ) ) , ( ( 2nd ` <. A , B >. ) .N ( 2nd ` <. C , D >. ) ) >. = <. ( ( A .N D ) +N ( C .N B ) ) , ( B .N D ) >. )
14 4 13 eqtrd 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. +pQ <. C , D >. ) = <. ( ( A .N D ) +N ( C .N B ) ) , ( B .N D ) >. )