Metamath Proof Explorer

Theorem dmmulsr

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

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

Proof

Step Hyp Ref Expression
1 df-mr 
 |-  .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 ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~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 ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~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 ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) } C_ ( R. X. R. )
4 2 3 eqsstri 
 |-  dom .R C_ ( R. X. R. )
5 0nsr 
 |-  -. (/) e. R.
6 mulclsr 
 |-  ( ( 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. )