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 ) } ) |
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 ) } ) |