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 10927
Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11064, 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 10805 . 2 class ยทP
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 cnp 10802 . . 3 class P
5 vw . . . . . . . 8 setvar ๐‘ค
65cv 1541 . . . . . . 7 class ๐‘ค
7 vv . . . . . . . . 9 setvar ๐‘ฃ
87cv 1541 . . . . . . . 8 class ๐‘ฃ
9 vu . . . . . . . . 9 setvar ๐‘ข
109cv 1541 . . . . . . . 8 class ๐‘ข
11 cmq 10799 . . . . . . . 8 class ยทQ
128, 10, 11co 7362 . . . . . . 7 class (๐‘ฃ ยทQ ๐‘ข)
136, 12wceq 1542 . . . . . 6 wff ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)
143cv 1541 . . . . . 6 class ๐‘ฆ
1513, 9, 14wrex 3074 . . . . 5 wff โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)
162cv 1541 . . . . 5 class ๐‘ฅ
1715, 7, 16wrex 3074 . . . 4 wff โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)
1817, 5cab 2714 . . 3 class {๐‘ค โˆฃ โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)}
192, 3, 4, 4, 18cmpo 7364 . 2 class (๐‘ฅ โˆˆ P, ๐‘ฆ โˆˆ P โ†ฆ {๐‘ค โˆฃ โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)})
201, 19wceq 1542 1 wff ยทP = (๐‘ฅ โˆˆ P, ๐‘ฆ โˆˆ P โ†ฆ {๐‘ค โˆฃ โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)})
Colors of variables: wff setvar class
This definition is referenced by:  mpv  10954  dmmp  10956  mulclprlem  10962  mulclpr  10963  mulasspr  10967  distrlem1pr  10968  distrlem4pr  10969  distrlem5pr  10970  1idpr  10972  reclem3pr  10992  reclem4pr  10993
  Copyright terms: Public domain W3C validator