Metamath Proof Explorer

Theorem addsrmo

Description: There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019)

Ref Expression
Assertion addsrmo 
|- ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )

Proof

Step Hyp Ref Expression
1 enrer 
 |-  ~R Er ( P. X. P. )
2 1 a1i 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> ~R Er ( P. X. P. ) )
3 prsrlem1 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> ( ( ( ( w e. P. /\ v e. P. ) /\ ( s e. P. /\ f e. P. ) ) /\ ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) ) /\ ( ( w +P. f ) = ( v +P. s ) /\ ( u +P. h ) = ( t +P. g ) ) ) )
4 addcmpblnr 
 |-  ( ( ( ( w e. P. /\ v e. P. ) /\ ( s e. P. /\ f e. P. ) ) /\ ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) ) -> ( ( ( w +P. f ) = ( v +P. s ) /\ ( u +P. h ) = ( t +P. g ) ) -> <. ( w +P. u ) , ( v +P. t ) >. ~R <. ( s +P. g ) , ( f +P. h ) >. ) )
5 4 imp 
 |-  ( ( ( ( ( w e. P. /\ v e. P. ) /\ ( s e. P. /\ f e. P. ) ) /\ ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) ) /\ ( ( w +P. f ) = ( v +P. s ) /\ ( u +P. h ) = ( t +P. g ) ) ) -> <. ( w +P. u ) , ( v +P. t ) >. ~R <. ( s +P. g ) , ( f +P. h ) >. )
6 3 5 syl 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> <. ( w +P. u ) , ( v +P. t ) >. ~R <. ( s +P. g ) , ( f +P. h ) >. )
7 2 6 erthi 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R )
8 7 adantrlr 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R )
9 8 adantrrr 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) ) -> [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R )
10 simprlr 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) ) -> z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R )
11 simprrr 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) ) -> q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R )
12 9 10 11 3eqtr4d 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) ) -> z = q )
13 12 expr 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> ( ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) -> z = q ) )
14 13 exlimdvv 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> ( E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) -> z = q ) )
15 14 exlimdvv 
 |-  ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> ( E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) -> z = q ) )
16 15 ex 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) -> ( E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) -> z = q ) ) )
17 16 exlimdvv 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> ( E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) -> ( E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) -> z = q ) ) )
18 17 exlimdvv 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) -> ( E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) -> z = q ) ) )
19 18 impd 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) -> z = q ) )
20 19 alrimivv 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> A. z A. q ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) -> z = q ) )
21 opeq12 
 |-  ( ( w = s /\ v = f ) -> <. w , v >. = <. s , f >. )
22 21 eceq1d 
 |-  ( ( w = s /\ v = f ) -> [ <. w , v >. ] ~R = [ <. s , f >. ] ~R )
23 22 eqeq2d 
 |-  ( ( w = s /\ v = f ) -> ( A = [ <. w , v >. ] ~R <-> A = [ <. s , f >. ] ~R ) )
24 23 anbi1d 
 |-  ( ( w = s /\ v = f ) -> ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) <-> ( A = [ <. s , f >. ] ~R /\ B = [ <. u , t >. ] ~R ) ) )
25 simpl 
 |-  ( ( w = s /\ v = f ) -> w = s )
26 25 oveq1d 
 |-  ( ( w = s /\ v = f ) -> ( w +P. u ) = ( s +P. u ) )
27 simpr 
 |-  ( ( w = s /\ v = f ) -> v = f )
28 27 oveq1d 
 |-  ( ( w = s /\ v = f ) -> ( v +P. t ) = ( f +P. t ) )
29 26 28 opeq12d 
 |-  ( ( w = s /\ v = f ) -> <. ( w +P. u ) , ( v +P. t ) >. = <. ( s +P. u ) , ( f +P. t ) >. )
30 29 eceq1d 
 |-  ( ( w = s /\ v = f ) -> [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R = [ <. ( s +P. u ) , ( f +P. t ) >. ] ~R )
31 30 eqeq2d 
 |-  ( ( w = s /\ v = f ) -> ( q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R <-> q = [ <. ( s +P. u ) , ( f +P. t ) >. ] ~R ) )
32 24 31 anbi12d 
 |-  ( ( w = s /\ v = f ) -> ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> ( ( A = [ <. s , f >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( s +P. u ) , ( f +P. t ) >. ] ~R ) ) )
33 opeq12 
 |-  ( ( u = g /\ t = h ) -> <. u , t >. = <. g , h >. )
34 33 eceq1d 
 |-  ( ( u = g /\ t = h ) -> [ <. u , t >. ] ~R = [ <. g , h >. ] ~R )
35 34 eqeq2d 
 |-  ( ( u = g /\ t = h ) -> ( B = [ <. u , t >. ] ~R <-> B = [ <. g , h >. ] ~R ) )
36 35 anbi2d 
 |-  ( ( u = g /\ t = h ) -> ( ( A = [ <. s , f >. ] ~R /\ B = [ <. u , t >. ] ~R ) <-> ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) )
37 simpl 
 |-  ( ( u = g /\ t = h ) -> u = g )
38 37 oveq2d 
 |-  ( ( u = g /\ t = h ) -> ( s +P. u ) = ( s +P. g ) )
39 simpr 
 |-  ( ( u = g /\ t = h ) -> t = h )
40 39 oveq2d 
 |-  ( ( u = g /\ t = h ) -> ( f +P. t ) = ( f +P. h ) )
41 38 40 opeq12d 
 |-  ( ( u = g /\ t = h ) -> <. ( s +P. u ) , ( f +P. t ) >. = <. ( s +P. g ) , ( f +P. h ) >. )
42 41 eceq1d 
 |-  ( ( u = g /\ t = h ) -> [ <. ( s +P. u ) , ( f +P. t ) >. ] ~R = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R )
43 42 eqeq2d 
 |-  ( ( u = g /\ t = h ) -> ( q = [ <. ( s +P. u ) , ( f +P. t ) >. ] ~R <-> q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) )
44 36 43 anbi12d 
 |-  ( ( u = g /\ t = h ) -> ( ( ( A = [ <. s , f >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( s +P. u ) , ( f +P. t ) >. ] ~R ) <-> ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) )
45 32 44 cbvex4vw 
 |-  ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) )
46 45 anbi2i 
 |-  ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) <-> ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) )
47 46 imbi1i 
 |-  ( ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> z = q ) <-> ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) -> z = q ) )
48 47 2albii 
 |-  ( A. z A. q ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> z = q ) <-> A. z A. q ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. s E. f E. g E. h ( ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) /\ q = [ <. ( s +P. g ) , ( f +P. h ) >. ] ~R ) ) -> z = q ) )
49 20 48 sylibr 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> A. z A. q ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> z = q ) )
50 eqeq1 
 |-  ( z = q -> ( z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R <-> q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )
51 50 anbi2d 
 |-  ( z = q -> ( ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
52 51 4exbidv 
 |-  ( z = q -> ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) )
53 52 mo4 
 |-  ( E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) <-> A. z A. q ( ( E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) /\ E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ q = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) ) -> z = q ) )
54 49 53 sylibr 
 |-  ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )