Metamath Proof Explorer

Theorem addcompq

Description: Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion addcompq 
|- ( A +pQ B ) = ( B +pQ A )

Proof

Step Hyp Ref Expression
1 addcompi 
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` B ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` B ) ) )
2 mulcompi 
 |-  ( ( 2nd ` A ) .N ( 2nd ` B ) ) = ( ( 2nd ` B ) .N ( 2nd ` A ) )
3 1 2 opeq12i 
 |-  <. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. = <. ( ( ( 1st ` B ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` A ) ) >.
4 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 ) ) >. )
5 addpipq2 
 |-  ( ( B e. ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> ( B +pQ A ) = <. ( ( ( 1st ` B ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` A ) ) >. )
6 5 ancoms 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( B +pQ A ) = <. ( ( ( 1st ` B ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) , ( ( 2nd ` B ) .N ( 2nd ` A ) ) >. )
7 3 4 6 3eqtr4a 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A +pQ B ) = ( B +pQ A ) )
8 addpqf 
 |-  +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
9 8 fdmi 
 |-  dom +pQ = ( ( N. X. N. ) X. ( N. X. N. ) )
10 9 ndmovcom 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A +pQ B ) = ( B +pQ A ) )
11 7 10 pm2.61i 
 |-  ( A +pQ B ) = ( B +pQ A )