Metamath Proof Explorer


Definition df-mp

Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-3.7 of Gleason p. 124. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion df-mp
|- .P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmp
 |-  .P.
1 vx
 |-  x
2 cnp
 |-  P.
3 vy
 |-  y
4 vw
 |-  w
5 vv
 |-  v
6 1 cv
 |-  x
7 vu
 |-  u
8 3 cv
 |-  y
9 4 cv
 |-  w
10 5 cv
 |-  v
11 cmq
 |-  .Q
12 7 cv
 |-  u
13 10 12 11 co
 |-  ( v .Q u )
14 9 13 wceq
 |-  w = ( v .Q u )
15 14 7 8 wrex
 |-  E. u e. y w = ( v .Q u )
16 15 5 6 wrex
 |-  E. v e. x E. u e. y w = ( v .Q u )
17 16 4 cab
 |-  { w | E. v e. x E. u e. y w = ( v .Q u ) }
18 1 3 2 2 17 cmpo
 |-  ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )
19 0 18 wceq
 |-  .P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )