Metamath Proof Explorer

Theorem prsrlem1

Description: Decomposing signed reals into positive reals. Lemma for addsrpr and mulsrpr . (Contributed by Jim Kingdon, 30-Dec-2019)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 enrer 
 |-  ~R Er ( P. X. P. )
2 erdm 
 |-  ( ~R Er ( P. X. P. ) -> dom ~R = ( P. X. P. ) )
3 1 2 ax-mp 
 |-  dom ~R = ( P. X. P. )
4 simprll 
 |-  ( ( ( 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 ) ) ) -> A = [ <. w , v >. ] ~R )
5 simpll 
 |-  ( ( ( 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 ) ) ) -> A e. ( ( P. X. P. ) /. ~R ) )
6 4 5 eqeltrrd 
 |-  ( ( ( 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 , v >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
7 ecelqsdm 
 |-  ( ( dom ~R = ( P. X. P. ) /\ [ <. w , v >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) -> <. w , v >. e. ( P. X. P. ) )
8 3 6 7 sylancr 
 |-  ( ( ( 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 , v >. e. ( P. X. P. ) )
9 opelxp 
 |-  ( <. w , v >. e. ( P. X. P. ) <-> ( w e. P. /\ v e. P. ) )
10 8 9 sylib 
 |-  ( ( ( 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. ) )
11 simprrl 
 |-  ( ( ( 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 ) ) ) -> A = [ <. s , f >. ] ~R )
12 11 5 eqeltrrd 
 |-  ( ( ( 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 ) ) ) -> [ <. s , f >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
13 ecelqsdm 
 |-  ( ( dom ~R = ( P. X. P. ) /\ [ <. s , f >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) -> <. s , f >. e. ( P. X. P. ) )
14 3 12 13 sylancr 
 |-  ( ( ( 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 ) ) ) -> <. s , f >. e. ( P. X. P. ) )
15 opelxp 
 |-  ( <. s , f >. e. ( P. X. P. ) <-> ( s e. P. /\ f e. P. ) )
16 14 15 sylib 
 |-  ( ( ( 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 ) ) ) -> ( s e. P. /\ f e. P. ) )
17 10 16 jca 
 |-  ( ( ( 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. ) ) )
18 simprlr 
 |-  ( ( ( 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 ) ) ) -> B = [ <. u , t >. ] ~R )
19 simplr 
 |-  ( ( ( 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 ) ) ) -> B e. ( ( P. X. P. ) /. ~R ) )
20 18 19 eqeltrrd 
 |-  ( ( ( 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 ) ) ) -> [ <. u , t >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
21 ecelqsdm 
 |-  ( ( dom ~R = ( P. X. P. ) /\ [ <. u , t >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) -> <. u , t >. e. ( P. X. P. ) )
22 3 20 21 sylancr 
 |-  ( ( ( 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 ) ) ) -> <. u , t >. e. ( P. X. P. ) )
23 opelxp 
 |-  ( <. u , t >. e. ( P. X. P. ) <-> ( u e. P. /\ t e. P. ) )
24 22 23 sylib 
 |-  ( ( ( 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 ) ) ) -> ( u e. P. /\ t e. P. ) )
25 simprrr 
 |-  ( ( ( 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 ) ) ) -> B = [ <. g , h >. ] ~R )
26 25 19 eqeltrrd 
 |-  ( ( ( 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 ) ) ) -> [ <. g , h >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
27 ecelqsdm 
 |-  ( ( dom ~R = ( P. X. P. ) /\ [ <. g , h >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) -> <. g , h >. e. ( P. X. P. ) )
28 3 26 27 sylancr 
 |-  ( ( ( 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 ) ) ) -> <. g , h >. e. ( P. X. P. ) )
29 opelxp 
 |-  ( <. g , h >. e. ( P. X. P. ) <-> ( g e. P. /\ h e. P. ) )
30 28 29 sylib 
 |-  ( ( ( 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 ) ) ) -> ( g e. P. /\ h e. P. ) )
31 24 30 jca 
 |-  ( ( ( 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 ) ) ) -> ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) )
32 4 11 eqtr3d 
 |-  ( ( ( 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 , v >. ] ~R = [ <. s , f >. ] ~R )
33 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. ) )
34 33 8 erth 
 |-  ( ( ( 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 , v >. ~R <. s , f >. <-> [ <. w , v >. ] ~R = [ <. s , f >. ] ~R ) )
35 32 34 mpbird 
 |-  ( ( ( 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 , v >. ~R <. s , f >. )
36 df-enr 
 |-  ~R = { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. a E. b E. c E. d ( ( x = <. a , b >. /\ y = <. c , d >. ) /\ ( a +P. d ) = ( b +P. c ) ) ) }
37 36 ecopoveq 
 |-  ( ( ( w e. P. /\ v e. P. ) /\ ( s e. P. /\ f e. P. ) ) -> ( <. w , v >. ~R <. s , f >. <-> ( w +P. f ) = ( v +P. s ) ) )
38 10 16 37 syl2anc 
 |-  ( ( ( 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 , v >. ~R <. s , f >. <-> ( w +P. f ) = ( v +P. s ) ) )
39 35 38 mpbid 
 |-  ( ( ( 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. f ) = ( v +P. s ) )
40 18 25 eqtr3d 
 |-  ( ( ( 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 ) ) ) -> [ <. u , t >. ] ~R = [ <. g , h >. ] ~R )
41 33 22 erth 
 |-  ( ( ( 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 ) ) ) -> ( <. u , t >. ~R <. g , h >. <-> [ <. u , t >. ] ~R = [ <. g , h >. ] ~R ) )
42 40 41 mpbird 
 |-  ( ( ( 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 ) ) ) -> <. u , t >. ~R <. g , h >. )
43 36 ecopoveq 
 |-  ( ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) -> ( <. u , t >. ~R <. g , h >. <-> ( u +P. h ) = ( t +P. g ) ) )
44 24 30 43 syl2anc 
 |-  ( ( ( 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 ) ) ) -> ( <. u , t >. ~R <. g , h >. <-> ( u +P. h ) = ( t +P. g ) ) )
45 42 44 mpbid 
 |-  ( ( ( 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 ) ) ) -> ( u +P. h ) = ( t +P. g ) )
46 39 45 jca 
 |-  ( ( ( 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. f ) = ( v +P. s ) /\ ( u +P. h ) = ( t +P. g ) ) )
47 17 31 46 jca31 
 |-  ( ( ( 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 ) ) ) )