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

Definition df-ply 25693
Description: Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.)
Assertion
Ref Expression
df-ply Poly = (๐‘ฅ โˆˆ ๐’ซ โ„‚ โ†ฆ {๐‘“ โˆฃ โˆƒ๐‘› โˆˆ โ„•0 โˆƒ๐‘Ž โˆˆ ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))})
Distinct variable group:   ๐‘“,๐‘Ž,๐‘˜,๐‘›,๐‘ฅ,๐‘ง

Detailed syntax breakdown of Definition df-ply
StepHypRef Expression
1 cply 25689 . 2 class Poly
2 vx . . 3 setvar ๐‘ฅ
3 cc 11104 . . . 4 class โ„‚
43cpw 4601 . . 3 class ๐’ซ โ„‚
5 vf . . . . . . . 8 setvar ๐‘“
65cv 1540 . . . . . . 7 class ๐‘“
7 vz . . . . . . . 8 setvar ๐‘ง
8 cc0 11106 . . . . . . . . . 10 class 0
9 vn . . . . . . . . . . 11 setvar ๐‘›
109cv 1540 . . . . . . . . . 10 class ๐‘›
11 cfz 13480 . . . . . . . . . 10 class ...
128, 10, 11co 7405 . . . . . . . . 9 class (0...๐‘›)
13 vk . . . . . . . . . . . 12 setvar ๐‘˜
1413cv 1540 . . . . . . . . . . 11 class ๐‘˜
15 va . . . . . . . . . . . 12 setvar ๐‘Ž
1615cv 1540 . . . . . . . . . . 11 class ๐‘Ž
1714, 16cfv 6540 . . . . . . . . . 10 class (๐‘Žโ€˜๐‘˜)
187cv 1540 . . . . . . . . . . 11 class ๐‘ง
19 cexp 14023 . . . . . . . . . . 11 class โ†‘
2018, 14, 19co 7405 . . . . . . . . . 10 class (๐‘งโ†‘๐‘˜)
21 cmul 11111 . . . . . . . . . 10 class ยท
2217, 20, 21co 7405 . . . . . . . . 9 class ((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))
2312, 22, 13csu 15628 . . . . . . . 8 class ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))
247, 3, 23cmpt 5230 . . . . . . 7 class (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
256, 24wceq 1541 . . . . . 6 wff ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
262cv 1540 . . . . . . . 8 class ๐‘ฅ
278csn 4627 . . . . . . . 8 class {0}
2826, 27cun 3945 . . . . . . 7 class (๐‘ฅ โˆช {0})
29 cn0 12468 . . . . . . 7 class โ„•0
30 cmap 8816 . . . . . . 7 class โ†‘m
3128, 29, 30co 7405 . . . . . 6 class ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)
3225, 15, 31wrex 3070 . . . . 5 wff โˆƒ๐‘Ž โˆˆ ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
3332, 9, 29wrex 3070 . . . 4 wff โˆƒ๐‘› โˆˆ โ„•0 โˆƒ๐‘Ž โˆˆ ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
3433, 5cab 2709 . . 3 class {๐‘“ โˆฃ โˆƒ๐‘› โˆˆ โ„•0 โˆƒ๐‘Ž โˆˆ ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))}
352, 4, 34cmpt 5230 . 2 class (๐‘ฅ โˆˆ ๐’ซ โ„‚ โ†ฆ {๐‘“ โˆฃ โˆƒ๐‘› โˆˆ โ„•0 โˆƒ๐‘Ž โˆˆ ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))})
361, 35wceq 1541 1 wff Poly = (๐‘ฅ โˆˆ ๐’ซ โ„‚ โ†ฆ {๐‘“ โˆฃ โˆƒ๐‘› โˆˆ โ„•0 โˆƒ๐‘Ž โˆˆ ((๐‘ฅ โˆช {0}) โ†‘m โ„•0)๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))})
Colors of variables: wff setvar class
This definition is referenced by:  plyval  25698  plybss  25699
  Copyright terms: Public domain W3C validator