Description: Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | dmmp | |- dom .P. = ( P. X. P. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mp | |- .P. = ( x e. P. , y e. P. |-> { z | E. u e. x E. v e. y z = ( u .Q v ) } ) |
|
2 | mulclnq | |- ( ( u e. Q. /\ v e. Q. ) -> ( u .Q v ) e. Q. ) |
|
3 | 1 2 | genpdm | |- dom .P. = ( P. X. P. ) |