MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpr Unicode version

Definition df-mpr 8675
Description: Define pre-multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8738, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
Assertion
Ref Expression
df-mpr  |-  .pR  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. )
)  /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ) ) }
Distinct variable group:    x, y, z, w, v, u, f

Detailed syntax breakdown of Definition df-mpr
StepHypRef Expression
1 cmpr 8482 . 2  class  .pR
2 vx . . . . . . 7  set  x
32cv 1627 . . . . . 6  class  x
4 cnp 8476 . . . . . . 7  class  P.
54, 4cxp 4686 . . . . . 6  class  ( P. 
X.  P. )
63, 5wcel 1688 . . . . 5  wff  x  e.  ( P.  X.  P. )
7 vy . . . . . . 7  set  y
87cv 1627 . . . . . 6  class  y
98, 5wcel 1688 . . . . 5  wff  y  e.  ( P.  X.  P. )
106, 9wa 360 . . . 4  wff  ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. ) )
11 vw . . . . . . . . . . . . 13  set  w
1211cv 1627 . . . . . . . . . . . 12  class  w
13 vv . . . . . . . . . . . . 13  set  v
1413cv 1627 . . . . . . . . . . . 12  class  v
1512, 14cop 3644 . . . . . . . . . . 11  class  <. w ,  v >.
163, 15wceq 1628 . . . . . . . . . 10  wff  x  = 
<. w ,  v >.
17 vu . . . . . . . . . . . . 13  set  u
1817cv 1627 . . . . . . . . . . . 12  class  u
19 vf . . . . . . . . . . . . 13  set  f
2019cv 1627 . . . . . . . . . . . 12  class  f
2118, 20cop 3644 . . . . . . . . . . 11  class  <. u ,  f >.
228, 21wceq 1628 . . . . . . . . . 10  wff  y  = 
<. u ,  f >.
2316, 22wa 360 . . . . . . . . 9  wff  ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )
24 vz . . . . . . . . . . 11  set  z
2524cv 1627 . . . . . . . . . 10  class  z
26 cmp 8479 . . . . . . . . . . . . 13  class  .P.
2712, 18, 26co 5819 . . . . . . . . . . . 12  class  ( w  .P.  u )
2814, 20, 26co 5819 . . . . . . . . . . . 12  class  ( v  .P.  f )
29 cpp 8478 . . . . . . . . . . . 12  class  +P.
3027, 28, 29co 5819 . . . . . . . . . . 11  class  ( ( w  .P.  u )  +P.  ( v  .P.  f ) )
3112, 20, 26co 5819 . . . . . . . . . . . 12  class  ( w  .P.  f )
3214, 18, 26co 5819 . . . . . . . . . . . 12  class  ( v  .P.  u )
3331, 32, 29co 5819 . . . . . . . . . . 11  class  ( ( w  .P.  f )  +P.  ( v  .P.  u ) )
3430, 33cop 3644 . . . . . . . . . 10  class  <. (
( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >.
3525, 34wceq 1628 . . . . . . . . 9  wff  z  = 
<. ( ( w  .P.  u )  +P.  (
v  .P.  f )
) ,  ( ( w  .P.  f )  +P.  ( v  .P.  u ) ) >.
3623, 35wa 360 . . . . . . . 8  wff  ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  /\  z  =  <. ( ( w  .P.  u )  +P.  ( v  .P.  f
) ) ,  ( ( w  .P.  f
)  +P.  ( v  .P.  u ) ) >.
)
3736, 19wex 1533 . . . . . . 7  wff  E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. )
3837, 17wex 1533 . . . . . 6  wff  E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. )
3938, 13wex 1533 . . . . 5  wff  E. v E. u E. f ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f
>. )  /\  z  =  <. ( ( w  .P.  u )  +P.  ( v  .P.  f
) ) ,  ( ( w  .P.  f
)  +P.  ( v  .P.  u ) ) >.
)
4039, 11wex 1533 . . . 4  wff  E. w E. v E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. )
4110, 40wa 360 . . 3  wff  ( ( x  e.  ( P. 
X.  P. )  /\  y  e.  ( P.  X.  P. ) )  /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ) )
4241, 2, 7, 24coprab 5820 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. ) )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ) ) }
431, 42wceq 1628 1  wff  .pR  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. )
)  /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v
>.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ) ) }
Colors of variables: wff set class
This definition is referenced by:  mulsrpr  8693
  Copyright terms: Public domain W3C validator