Metamath Proof Explorer

Theorem addsrpr

Description: Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995) (Revised by Mario Carneiro, 12-Aug-2015) (New usage is discouraged.)

Ref Expression
Assertion addsrpr 
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R +R [ <. C , D >. ] ~R ) = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R )

Proof

Step Hyp Ref Expression
1 opelxpi 
 |-  ( ( A e. P. /\ B e. P. ) -> <. A , B >. e. ( P. X. P. ) )
2 enrex 
 |-  ~R e. _V
3 2 ecelqsi 
 |-  ( <. A , B >. e. ( P. X. P. ) -> [ <. A , B >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
4 1 3 syl 
 |-  ( ( A e. P. /\ B e. P. ) -> [ <. A , B >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
5 opelxpi 
 |-  ( ( C e. P. /\ D e. P. ) -> <. C , D >. e. ( P. X. P. ) )
6 2 ecelqsi 
 |-  ( <. C , D >. e. ( P. X. P. ) -> [ <. C , D >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
7 5 6 syl 
 |-  ( ( C e. P. /\ D e. P. ) -> [ <. C , D >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
8 4 7 anim12i 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R e. ( ( P. X. P. ) /. ~R ) /\ [ <. C , D >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) )
9 eqid 
 |-  [ <. A , B >. ] ~R = [ <. A , B >. ] ~R
10 eqid 
 |-  [ <. C , D >. ] ~R = [ <. C , D >. ] ~R
11 9 10 pm3.2i 
 |-  ( [ <. A , B >. ] ~R = [ <. A , B >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R )
12 eqid 
 |-  [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R
13 opeq12 
 |-  ( ( w = A /\ v = B ) -> <. w , v >. = <. A , B >. )
14 13 eceq1d 
 |-  ( ( w = A /\ v = B ) -> [ <. w , v >. ] ~R = [ <. A , B >. ] ~R )
15 14 eqeq2d 
 |-  ( ( w = A /\ v = B ) -> ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R <-> [ <. A , B >. ] ~R = [ <. A , B >. ] ~R ) )
16 15 anbi1d 
 |-  ( ( w = A /\ v = B ) -> ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) <-> ( [ <. A , B >. ] ~R = [ <. A , B >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) ) )
17 simpl 
 |-  ( ( w = A /\ v = B ) -> w = A )
18 17 oveq1d 
 |-  ( ( w = A /\ v = B ) -> ( w +P. C ) = ( A +P. C ) )
19 simpr 
 |-  ( ( w = A /\ v = B ) -> v = B )
20 19 oveq1d 
 |-  ( ( w = A /\ v = B ) -> ( v +P. D ) = ( B +P. D ) )
21 18 20 opeq12d 
 |-  ( ( w = A /\ v = B ) -> <. ( w +P. C ) , ( v +P. D ) >. = <. ( A +P. C ) , ( B +P. D ) >. )
22 21 eceq1d 
 |-  ( ( w = A /\ v = B ) -> [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R )
23 22 eqeq2d 
 |-  ( ( w = A /\ v = B ) -> ( [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R <-> [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) )
24 16 23 anbi12d 
 |-  ( ( w = A /\ v = B ) -> ( ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R ) <-> ( ( [ <. A , B >. ] ~R = [ <. A , B >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) ) )
25 24 spc2egv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( ( [ <. A , B >. ] ~R = [ <. A , B >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> E. w E. v ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R ) ) )
26 opeq12 
 |-  ( ( u = C /\ t = D ) -> <. u , t >. = <. C , D >. )
27 26 eceq1d 
 |-  ( ( u = C /\ t = D ) -> [ <. u , t >. ] ~R = [ <. C , D >. ] ~R )
28 27 eqeq2d 
 |-  ( ( u = C /\ t = D ) -> ( [ <. C , D >. ] ~R = [ <. u , t >. ] ~R <-> [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) )
29 28 anbi2d 
 |-  ( ( u = C /\ t = D ) -> ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) <-> ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) ) )
30 simpl 
 |-  ( ( u = C /\ t = D ) -> u = C )
31 30 oveq2d 
 |-  ( ( u = C /\ t = D ) -> ( w +P. u ) = ( w +P. C ) )
32 simpr 
 |-  ( ( u = C /\ t = D ) -> t = D )
33 32 oveq2d 
 |-  ( ( u = C /\ t = D ) -> ( v +P. t ) = ( v +P. D ) )
34 31 33 opeq12d 
 |-  ( ( u = C /\ t = D ) -> <. ( w +P. u ) , ( v +P. t ) >. = <. ( w +P. C ) , ( v +P. D ) >. )
35 34 eceq1d 
 |-  ( ( u = C /\ t = D ) -> [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R )
36 35 eqeq2d 
 |-  ( ( u = C /\ t = D ) -> ( [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R <-> [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R ) )
37 29 36 anbi12d 
 |-  ( ( u = C /\ t = D ) -> ( ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R ) ) )
38 37 spc2egv 
 |-  ( ( C e. P. /\ D e. P. ) -> ( ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R ) -> E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
39 38 2eximdv 
 |-  ( ( C e. P. /\ D e. P. ) -> ( E. w E. v ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. C ) , ( v +P. D ) >. ] ~R ) -> E. w E. v E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
40 25 39 sylan9 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( ( ( [ <. A , B >. ] ~R = [ <. A , B >. ] ~R /\ [ <. C , D >. ] ~R = [ <. C , D >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> E. w E. v E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
41 11 12 40 mp2ani 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> E. w E. v E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )
42 ecexg 
 |-  ( ~R e. _V -> [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R e. _V )
43 2 42 ax-mp 
 |-  [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R e. _V
44 simp1 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> x = [ <. A , B >. ] ~R )
45 44 eqeq1d 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> ( x = [ <. w , v >. ] ~R <-> [ <. A , B >. ] ~R = [ <. w , v >. ] ~R ) )
46 simp2 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> y = [ <. C , D >. ] ~R )
47 46 eqeq1d 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> ( y = [ <. u , t >. ] ~R <-> [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) )
48 45 47 anbi12d 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) <-> ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) ) )
49 simp3 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R )
50 49 eqeq1d 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> ( z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R <-> [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )
51 48 50 anbi12d 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> ( ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
52 51 4exbidv 
 |-  ( ( x = [ <. A , B >. ] ~R /\ y = [ <. C , D >. ] ~R /\ z = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) -> ( E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> E. w E. v E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
53 addsrmo 
 |-  ( ( x e. ( ( P. X. P. ) /. ~R ) /\ y e. ( ( P. X. P. ) /. ~R ) ) -> E* z E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )
54 df-plr 
 |-  +R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) }
55 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
56 55 eleq2i 
 |-  ( x e. R. <-> x e. ( ( P. X. P. ) /. ~R ) )
57 55 eleq2i 
 |-  ( y e. R. <-> y e. ( ( P. X. P. ) /. ~R ) )
58 56 57 anbi12i 
 |-  ( ( x e. R. /\ y e. R. ) <-> ( x e. ( ( P. X. P. ) /. ~R ) /\ y e. ( ( P. X. P. ) /. ~R ) ) )
59 58 anbi1i 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) <-> ( ( x e. ( ( P. X. P. ) /. ~R ) /\ y e. ( ( P. X. P. ) /. ~R ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
60 59 oprabbii 
 |-  { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) } = { <. <. x , y >. , z >. | ( ( x e. ( ( P. X. P. ) /. ~R ) /\ y e. ( ( P. X. P. ) /. ~R ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) }
61 54 60 eqtri 
 |-  +R = { <. <. x , y >. , z >. | ( ( x e. ( ( P. X. P. ) /. ~R ) /\ y e. ( ( P. X. P. ) /. ~R ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) }
62 52 53 61 ovig 
 |-  ( ( [ <. A , B >. ] ~R e. ( ( P. X. P. ) /. ~R ) /\ [ <. C , D >. ] ~R e. ( ( P. X. P. ) /. ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R e. _V ) -> ( E. w E. v E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) -> ( [ <. A , B >. ] ~R +R [ <. C , D >. ] ~R ) = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) )
63 43 62 mp3an3 
 |-  ( ( [ <. A , B >. ] ~R e. ( ( P. X. P. ) /. ~R ) /\ [ <. C , D >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) -> ( E. w E. v E. u E. t ( ( [ <. A , B >. ] ~R = [ <. w , v >. ] ~R /\ [ <. C , D >. ] ~R = [ <. u , t >. ] ~R ) /\ [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) -> ( [ <. A , B >. ] ~R +R [ <. C , D >. ] ~R ) = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R ) )
64 8 41 63 sylc 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R +R [ <. C , D >. ] ~R ) = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R )