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 10978
Description: Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11115, 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 10856 . 2 class ยทP
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 cnp 10853 . . 3 class P
5 vw . . . . . . . 8 setvar ๐‘ค
65cv 1540 . . . . . . 7 class ๐‘ค
7 vv . . . . . . . . 9 setvar ๐‘ฃ
87cv 1540 . . . . . . . 8 class ๐‘ฃ
9 vu . . . . . . . . 9 setvar ๐‘ข
109cv 1540 . . . . . . . 8 class ๐‘ข
11 cmq 10850 . . . . . . . 8 class ยทQ
128, 10, 11co 7408 . . . . . . 7 class (๐‘ฃ ยทQ ๐‘ข)
136, 12wceq 1541 . . . . . 6 wff ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)
143cv 1540 . . . . . 6 class ๐‘ฆ
1513, 9, 14wrex 3070 . . . . 5 wff โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)
162cv 1540 . . . . 5 class ๐‘ฅ
1715, 7, 16wrex 3070 . . . 4 wff โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)
1817, 5cab 2709 . . 3 class {๐‘ค โˆฃ โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)}
192, 3, 4, 4, 18cmpo 7410 . 2 class (๐‘ฅ โˆˆ P, ๐‘ฆ โˆˆ P โ†ฆ {๐‘ค โˆฃ โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)})
201, 19wceq 1541 1 wff ยทP = (๐‘ฅ โˆˆ P, ๐‘ฆ โˆˆ P โ†ฆ {๐‘ค โˆฃ โˆƒ๐‘ฃ โˆˆ ๐‘ฅ โˆƒ๐‘ข โˆˆ ๐‘ฆ ๐‘ค = (๐‘ฃ ยทQ ๐‘ข)})
Colors of variables: wff setvar class
This definition is referenced by:  mpv  11005  dmmp  11007  mulclprlem  11013  mulclpr  11014  mulasspr  11018  distrlem1pr  11019  distrlem4pr  11020  distrlem5pr  11021  1idpr  11023  reclem3pr  11043  reclem4pr  11044
  Copyright terms: Public domain W3C validator