MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mp Structured version   Visualization version   GIF version

Definition df-mp 9662
Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9798, 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.)
Assertion
Ref Expression
df-mp ·P = (𝑥P, 𝑦P ↦ {𝑤 ∣ ∃𝑣𝑥𝑢𝑦 𝑤 = (𝑣 ·Q 𝑢)})
Distinct variable group:   𝑥,𝑦,𝑤,𝑣,𝑢

Detailed syntax breakdown of Definition df-mp
StepHypRef Expression
1 cmp 9540 . 2 class ·P
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cnp 9537 . . 3 class P
5 vw . . . . . . . 8 setvar 𝑤
65cv 1473 . . . . . . 7 class 𝑤
7 vv . . . . . . . . 9 setvar 𝑣
87cv 1473 . . . . . . . 8 class 𝑣
9 vu . . . . . . . . 9 setvar 𝑢
109cv 1473 . . . . . . . 8 class 𝑢
11 cmq 9534 . . . . . . . 8 class ·Q
128, 10, 11co 6527 . . . . . . 7 class (𝑣 ·Q 𝑢)
136, 12wceq 1474 . . . . . 6 wff 𝑤 = (𝑣 ·Q 𝑢)
143cv 1473 . . . . . 6 class 𝑦
1513, 9, 14wrex 2896 . . . . 5 wff 𝑢𝑦 𝑤 = (𝑣 ·Q 𝑢)
162cv 1473 . . . . 5 class 𝑥
1715, 7, 16wrex 2896 . . . 4 wff 𝑣𝑥𝑢𝑦 𝑤 = (𝑣 ·Q 𝑢)
1817, 5cab 2595 . . 3 class {𝑤 ∣ ∃𝑣𝑥𝑢𝑦 𝑤 = (𝑣 ·Q 𝑢)}
192, 3, 4, 4, 18cmpt2 6529 . 2 class (𝑥P, 𝑦P ↦ {𝑤 ∣ ∃𝑣𝑥𝑢𝑦 𝑤 = (𝑣 ·Q 𝑢)})
201, 19wceq 1474 1 wff ·P = (𝑥P, 𝑦P ↦ {𝑤 ∣ ∃𝑣𝑥𝑢𝑦 𝑤 = (𝑣 ·Q 𝑢)})
Colors of variables: wff setvar class
This definition is referenced by:  mpv  9689  dmmp  9691  mulclprlem  9697  mulclpr  9698  mulasspr  9702  distrlem1pr  9703  distrlem4pr  9704  distrlem5pr  9705  1idpr  9707  reclem3pr  9727  reclem4pr  9728
  Copyright terms: Public domain W3C validator