This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0idsr

Description: The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion 0idsr 
|- ( A e. R. -> ( A +R 0R ) = A )

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 oveq1 
 |-  ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R +R 0R ) = ( A +R 0R ) )
3 id 
 |-  ( [ <. x , y >. ] ~R = A -> [ <. x , y >. ] ~R = A )
4 2 3 eqeq12d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R +R 0R ) = [ <. x , y >. ] ~R <-> ( A +R 0R ) = A ) )
5 df-0r 
 |-  0R = [ <. 1P , 1P >. ] ~R
6 5 oveq2i 
 |-  ( [ <. x , y >. ] ~R +R 0R ) = ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R )
7 1pr 
 |-  1P e. P.
8 addsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( 1P e. P. /\ 1P e. P. ) ) -> ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R )
9 7 7 8 mpanr12 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R )
10 addclpr 
 |-  ( ( x e. P. /\ 1P e. P. ) -> ( x +P. 1P ) e. P. )
11 7 10 mpan2 
 |-  ( x e. P. -> ( x +P. 1P ) e. P. )
12 addclpr 
 |-  ( ( y e. P. /\ 1P e. P. ) -> ( y +P. 1P ) e. P. )
13 7 12 mpan2 
 |-  ( y e. P. -> ( y +P. 1P ) e. P. )
14 11 13 anim12i 
 |-  ( ( x e. P. /\ y e. P. ) -> ( ( x +P. 1P ) e. P. /\ ( y +P. 1P ) e. P. ) )
15 vex 
 |-  x e. _V
16 vex 
 |-  y e. _V
17 7 elexi 
 |-  1P e. _V
18 addcompr 
 |-  ( z +P. w ) = ( w +P. z )
19 addasspr 
 |-  ( ( z +P. w ) +P. v ) = ( z +P. ( w +P. v ) )
20 15 16 17 18 19 caov12 
 |-  ( x +P. ( y +P. 1P ) ) = ( y +P. ( x +P. 1P ) )
21 enreceq 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( ( x +P. 1P ) e. P. /\ ( y +P. 1P ) e. P. ) ) -> ( [ <. x , y >. ] ~R = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R <-> ( x +P. ( y +P. 1P ) ) = ( y +P. ( x +P. 1P ) ) ) )
22 20 21 mpbiri 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( ( x +P. 1P ) e. P. /\ ( y +P. 1P ) e. P. ) ) -> [ <. x , y >. ] ~R = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R )
23 14 22 mpdan 
 |-  ( ( x e. P. /\ y e. P. ) -> [ <. x , y >. ] ~R = [ <. ( x +P. 1P ) , ( y +P. 1P ) >. ] ~R )
24 9 23 eqtr4d 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R +R [ <. 1P , 1P >. ] ~R ) = [ <. x , y >. ] ~R )
25 6 24 eqtrid 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R +R 0R ) = [ <. x , y >. ] ~R )
26 1 4 25 ecoptocl 
 |-  ( A e. R. -> ( A +R 0R ) = A )