Metamath Proof Explorer

Theorem addcmpblnr

Description: Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion addcmpblnr 
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. ) )

Proof

Step Hyp Ref Expression
1 oveq12 
 |-  ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( A +P. D ) +P. ( F +P. S ) ) = ( ( B +P. C ) +P. ( G +P. R ) ) )
2 addclpr 
 |-  ( ( A e. P. /\ F e. P. ) -> ( A +P. F ) e. P. )
3 addclpr 
 |-  ( ( B e. P. /\ G e. P. ) -> ( B +P. G ) e. P. )
4 2 3 anim12i 
 |-  ( ( ( A e. P. /\ F e. P. ) /\ ( B e. P. /\ G e. P. ) ) -> ( ( A +P. F ) e. P. /\ ( B +P. G ) e. P. ) )
5 4 an4s 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( F e. P. /\ G e. P. ) ) -> ( ( A +P. F ) e. P. /\ ( B +P. G ) e. P. ) )
6 addclpr 
 |-  ( ( C e. P. /\ R e. P. ) -> ( C +P. R ) e. P. )
7 addclpr 
 |-  ( ( D e. P. /\ S e. P. ) -> ( D +P. S ) e. P. )
8 6 7 anim12i 
 |-  ( ( ( C e. P. /\ R e. P. ) /\ ( D e. P. /\ S e. P. ) ) -> ( ( C +P. R ) e. P. /\ ( D +P. S ) e. P. ) )
9 8 an4s 
 |-  ( ( ( C e. P. /\ D e. P. ) /\ ( R e. P. /\ S e. P. ) ) -> ( ( C +P. R ) e. P. /\ ( D +P. S ) e. P. ) )
10 5 9 anim12i 
 |-  ( ( ( ( A e. P. /\ B e. P. ) /\ ( F e. P. /\ G e. P. ) ) /\ ( ( C e. P. /\ D e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. F ) e. P. /\ ( B +P. G ) e. P. ) /\ ( ( C +P. R ) e. P. /\ ( D +P. S ) e. P. ) ) )
11 10 an4s 
 |-  ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. F ) e. P. /\ ( B +P. G ) e. P. ) /\ ( ( C +P. R ) e. P. /\ ( D +P. S ) e. P. ) ) )
12 enrbreq 
 |-  ( ( ( ( A +P. F ) e. P. /\ ( B +P. G ) e. P. ) /\ ( ( C +P. R ) e. P. /\ ( D +P. S ) e. P. ) ) -> ( <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. <-> ( ( A +P. F ) +P. ( D +P. S ) ) = ( ( B +P. G ) +P. ( C +P. R ) ) ) )
13 11 12 syl 
 |-  ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. <-> ( ( A +P. F ) +P. ( D +P. S ) ) = ( ( B +P. G ) +P. ( C +P. R ) ) ) )
14 addcompr 
 |-  ( F +P. D ) = ( D +P. F )
15 14 oveq1i 
 |-  ( ( F +P. D ) +P. S ) = ( ( D +P. F ) +P. S )
16 addasspr 
 |-  ( ( F +P. D ) +P. S ) = ( F +P. ( D +P. S ) )
17 addasspr 
 |-  ( ( D +P. F ) +P. S ) = ( D +P. ( F +P. S ) )
18 15 16 17 3eqtr3i 
 |-  ( F +P. ( D +P. S ) ) = ( D +P. ( F +P. S ) )
19 18 oveq2i 
 |-  ( A +P. ( F +P. ( D +P. S ) ) ) = ( A +P. ( D +P. ( F +P. S ) ) )
20 addasspr 
 |-  ( ( A +P. F ) +P. ( D +P. S ) ) = ( A +P. ( F +P. ( D +P. S ) ) )
21 addasspr 
 |-  ( ( A +P. D ) +P. ( F +P. S ) ) = ( A +P. ( D +P. ( F +P. S ) ) )
22 19 20 21 3eqtr4i 
 |-  ( ( A +P. F ) +P. ( D +P. S ) ) = ( ( A +P. D ) +P. ( F +P. S ) )
23 addcompr 
 |-  ( G +P. C ) = ( C +P. G )
24 23 oveq1i 
 |-  ( ( G +P. C ) +P. R ) = ( ( C +P. G ) +P. R )
25 addasspr 
 |-  ( ( G +P. C ) +P. R ) = ( G +P. ( C +P. R ) )
26 addasspr 
 |-  ( ( C +P. G ) +P. R ) = ( C +P. ( G +P. R ) )
27 24 25 26 3eqtr3i 
 |-  ( G +P. ( C +P. R ) ) = ( C +P. ( G +P. R ) )
28 27 oveq2i 
 |-  ( B +P. ( G +P. ( C +P. R ) ) ) = ( B +P. ( C +P. ( G +P. R ) ) )
29 addasspr 
 |-  ( ( B +P. G ) +P. ( C +P. R ) ) = ( B +P. ( G +P. ( C +P. R ) ) )
30 addasspr 
 |-  ( ( B +P. C ) +P. ( G +P. R ) ) = ( B +P. ( C +P. ( G +P. R ) ) )
31 28 29 30 3eqtr4i 
 |-  ( ( B +P. G ) +P. ( C +P. R ) ) = ( ( B +P. C ) +P. ( G +P. R ) )
32 22 31 eqeq12i 
 |-  ( ( ( A +P. F ) +P. ( D +P. S ) ) = ( ( B +P. G ) +P. ( C +P. R ) ) <-> ( ( A +P. D ) +P. ( F +P. S ) ) = ( ( B +P. C ) +P. ( G +P. R ) ) )
33 13 32 bitrdi 
 |-  ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. <-> ( ( A +P. D ) +P. ( F +P. S ) ) = ( ( B +P. C ) +P. ( G +P. R ) ) ) )
34 1 33 imbitrrid 
 |-  ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. ) )