Metamath Proof Explorer

Theorem map2psrpr

Description: Equivalence for positive signed real. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypothesis map2psrpr.2 
|- C e. R.
Assertion map2psrpr 
|- ( ( C +R -1R )  E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A )

Proof

Step Hyp Ref Expression
1 map2psrpr.2 
 |-  C e. R.
2 ltrelsr 
 |-
3 2 brel 
 |-  ( ( C +R -1R )  ( ( C +R -1R ) e. R. /\ A e. R. ) )
4 3 simprd 
 |-  ( ( C +R -1R )  A e. R. )
5 ltasr 
 |-  ( C e. R. -> ( -1R  ( C +R -1R )
6 1 5 ax-mp 
 |-  ( -1R  ( C +R -1R )
7 pn0sr 
 |-  ( C e. R. -> ( C +R ( C .R -1R ) ) = 0R )
8 1 7 ax-mp 
 |-  ( C +R ( C .R -1R ) ) = 0R
9 8 oveq1i 
 |-  ( ( C +R ( C .R -1R ) ) +R A ) = ( 0R +R A )
10 addasssr 
 |-  ( ( C +R ( C .R -1R ) ) +R A ) = ( C +R ( ( C .R -1R ) +R A ) )
11 addcomsr 
 |-  ( 0R +R A ) = ( A +R 0R )
12 9 10 11 3eqtr3i 
 |-  ( C +R ( ( C .R -1R ) +R A ) ) = ( A +R 0R )
13 0idsr 
 |-  ( A e. R. -> ( A +R 0R ) = A )
14 12 13 syl5eq 
 |-  ( A e. R. -> ( C +R ( ( C .R -1R ) +R A ) ) = A )
15 14 breq2d 
 |-  ( A e. R. -> ( ( C +R -1R )  ( C +R -1R )
16 6 15 syl5bb 
 |-  ( A e. R. -> ( -1R  ( C +R -1R )
17 m1r 
 |-  -1R e. R.
18 mulclsr 
 |-  ( ( C e. R. /\ -1R e. R. ) -> ( C .R -1R ) e. R. )
19 1 17 18 mp2an 
 |-  ( C .R -1R ) e. R.
20 addclsr 
 |-  ( ( ( C .R -1R ) e. R. /\ A e. R. ) -> ( ( C .R -1R ) +R A ) e. R. )
21 19 20 mpan 
 |-  ( A e. R. -> ( ( C .R -1R ) +R A ) e. R. )
22 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
23 breq2 
 |-  ( [ <. y , z >. ] ~R = ( ( C .R -1R ) +R A ) -> ( -1R . ] ~R <-> -1R
24 eqeq2 
 |-  ( [ <. y , z >. ] ~R = ( ( C .R -1R ) +R A ) -> ( [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) ) )
25 24 rexbidv 
 |-  ( [ <. y , z >. ] ~R = ( ( C .R -1R ) +R A ) -> ( E. x e. P. [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> E. x e. P. [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) ) )
26 23 25 imbi12d 
 |-  ( [ <. y , z >. ] ~R = ( ( C .R -1R ) +R A ) -> ( ( -1R . ] ~R -> E. x e. P. [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R ) <-> ( -1R  E. x e. P. [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) ) ) )
27 df-m1r 
 |-  -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
28 27 breq1i 
 |-  ( -1R . ] ~R <-> [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R )
29 addasspr 
 |-  ( ( 1P +P. 1P ) +P. y ) = ( 1P +P. ( 1P +P. y ) )
30 29 breq2i 
 |-  ( ( 1P +P. z ) 
 ( 1P +P. z )
31 ltsrpr 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R <-> ( 1P +P. z )
32 1pr 
 |-  1P e. P.
33 ltapr 
 |-  ( 1P e. P. -> ( z 
 ( 1P +P. z )
34 32 33 ax-mp 
 |-  ( z 
 ( 1P +P. z )
35 30 31 34 3bitr4i 
 |-  ( [ <. 1P , ( 1P +P. 1P ) >. ] ~R . ] ~R <-> z
36 28 35 bitri 
 |-  ( -1R . ] ~R <-> z
37 ltexpri 
 |-  ( z 
 E. x e. P. ( z +P. x ) = ( 1P +P. y ) )
38 36 37 sylbi 
 |-  ( -1R . ] ~R -> E. x e. P. ( z +P. x ) = ( 1P +P. y ) )
39 enreceq 
 |-  ( ( ( x e. P. /\ 1P e. P. ) /\ ( y e. P. /\ z e. P. ) ) -> ( [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> ( x +P. z ) = ( 1P +P. y ) ) )
40 32 39 mpanl2 
 |-  ( ( x e. P. /\ ( y e. P. /\ z e. P. ) ) -> ( [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> ( x +P. z ) = ( 1P +P. y ) ) )
41 addcompr 
 |-  ( z +P. x ) = ( x +P. z )
42 41 eqeq1i 
 |-  ( ( z +P. x ) = ( 1P +P. y ) <-> ( x +P. z ) = ( 1P +P. y ) )
43 40 42 bitr4di 
 |-  ( ( x e. P. /\ ( y e. P. /\ z e. P. ) ) -> ( [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> ( z +P. x ) = ( 1P +P. y ) ) )
44 43 ancoms 
 |-  ( ( ( y e. P. /\ z e. P. ) /\ x e. P. ) -> ( [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> ( z +P. x ) = ( 1P +P. y ) ) )
45 44 rexbidva 
 |-  ( ( y e. P. /\ z e. P. ) -> ( E. x e. P. [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R <-> E. x e. P. ( z +P. x ) = ( 1P +P. y ) ) )
46 38 45 syl5ibr 
 |-  ( ( y e. P. /\ z e. P. ) -> ( -1R . ] ~R -> E. x e. P. [ <. x , 1P >. ] ~R = [ <. y , z >. ] ~R ) )
47 22 26 46 ecoptocl 
 |-  ( ( ( C .R -1R ) +R A ) e. R. -> ( -1R  E. x e. P. [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) ) )
48 21 47 syl 
 |-  ( A e. R. -> ( -1R  E. x e. P. [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) ) )
49 oveq2 
 |-  ( [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) -> ( C +R [ <. x , 1P >. ] ~R ) = ( C +R ( ( C .R -1R ) +R A ) ) )
50 49 14 sylan9eqr 
 |-  ( ( A e. R. /\ [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) ) -> ( C +R [ <. x , 1P >. ] ~R ) = A )
51 50 ex 
 |-  ( A e. R. -> ( [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) -> ( C +R [ <. x , 1P >. ] ~R ) = A ) )
52 51 reximdv 
 |-  ( A e. R. -> ( E. x e. P. [ <. x , 1P >. ] ~R = ( ( C .R -1R ) +R A ) -> E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A ) )
53 48 52 syld 
 |-  ( A e. R. -> ( -1R  E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A ) )
54 16 53 sylbird 
 |-  ( A e. R. -> ( ( C +R -1R )  E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A ) )
55 4 54 mpcom 
 |-  ( ( C +R -1R )  E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A )
56 1 mappsrpr 
 |-  ( ( C +R -1R ) . ] ~R ) <-> x e. P. )
57 breq2 
 |-  ( ( C +R [ <. x , 1P >. ] ~R ) = A -> ( ( C +R -1R ) . ] ~R ) <-> ( C +R -1R )
58 56 57 bitr3id 
 |-  ( ( C +R [ <. x , 1P >. ] ~R ) = A -> ( x e. P. <-> ( C +R -1R )
59 58 biimpac 
 |-  ( ( x e. P. /\ ( C +R [ <. x , 1P >. ] ~R ) = A ) -> ( C +R -1R )
60 59 rexlimiva 
 |-  ( E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A -> ( C +R -1R )
61 55 60 impbii 
 |-  ( ( C +R -1R )  E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A )