Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-itgo Structured version   Visualization version   GIF version

Definition df-itgo 41529
Description: A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 41532. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Assertion
Ref Expression
df-itgo IntgOver = (𝑠 ∈ 𝒫 β„‚ ↦ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘ ∈ (Polyβ€˜π‘ )((π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1)})
Distinct variable group:   π‘₯,𝑝,𝑠

Detailed syntax breakdown of Definition df-itgo
StepHypRef Expression
1 citgo 41527 . 2 class IntgOver
2 vs . . 3 setvar 𝑠
3 cc 11054 . . . 4 class β„‚
43cpw 4561 . . 3 class 𝒫 β„‚
5 vx . . . . . . . . 9 setvar π‘₯
65cv 1541 . . . . . . . 8 class π‘₯
7 vp . . . . . . . . 9 setvar 𝑝
87cv 1541 . . . . . . . 8 class 𝑝
96, 8cfv 6497 . . . . . . 7 class (π‘β€˜π‘₯)
10 cc0 11056 . . . . . . 7 class 0
119, 10wceq 1542 . . . . . 6 wff (π‘β€˜π‘₯) = 0
12 cdgr 25564 . . . . . . . . 9 class deg
138, 12cfv 6497 . . . . . . . 8 class (degβ€˜π‘)
14 ccoe 25563 . . . . . . . . 9 class coeff
158, 14cfv 6497 . . . . . . . 8 class (coeffβ€˜π‘)
1613, 15cfv 6497 . . . . . . 7 class ((coeffβ€˜π‘)β€˜(degβ€˜π‘))
17 c1 11057 . . . . . . 7 class 1
1816, 17wceq 1542 . . . . . 6 wff ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1
1911, 18wa 397 . . . . 5 wff ((π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1)
202cv 1541 . . . . . 6 class 𝑠
21 cply 25561 . . . . . 6 class Poly
2220, 21cfv 6497 . . . . 5 class (Polyβ€˜π‘ )
2319, 7, 22wrex 3070 . . . 4 wff βˆƒπ‘ ∈ (Polyβ€˜π‘ )((π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1)
2423, 5, 3crab 3406 . . 3 class {π‘₯ ∈ β„‚ ∣ βˆƒπ‘ ∈ (Polyβ€˜π‘ )((π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1)}
252, 4, 24cmpt 5189 . 2 class (𝑠 ∈ 𝒫 β„‚ ↦ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘ ∈ (Polyβ€˜π‘ )((π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1)})
261, 25wceq 1542 1 wff IntgOver = (𝑠 ∈ 𝒫 β„‚ ↦ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘ ∈ (Polyβ€˜π‘ )((π‘β€˜π‘₯) = 0 ∧ ((coeffβ€˜π‘)β€˜(degβ€˜π‘)) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  itgoval  41531  itgocn  41534
  Copyright terms: Public domain W3C validator