Metamath Proof Explorer

Theorem dmaddsr

Description: Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion dmaddsr 
|- dom +R = ( R. X. R. )

Proof

Step Hyp Ref Expression
1 df-plr 
 |-  +R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }
2 1 dmeqi 
 |-  dom +R = dom { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }
3 dmoprabss 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) } C_ ( R. X. R. )
4 2 3 eqsstri 
 |-  dom +R C_ ( R. X. R. )
5 0nsr 
 |-  -. (/) e. R.
6 addclsr 
 |-  ( ( x e. R. /\ y e. R. ) -> ( x +R y ) e. R. )
7 5 6 oprssdm 
 |-  ( R. X. R. ) C_ dom +R
8 4 7 eqssi 
 |-  dom +R = ( R. X. R. )