Metamath Proof Explorer


Definition df-itgo

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 . 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)

Ref Expression
Assertion df-itgo IntgOver = s 𝒫 x | p Poly s p x = 0 coeff p deg p = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 citgo class IntgOver
1 vs setvar s
2 cc class
3 2 cpw class 𝒫
4 vx setvar x
5 vp setvar p
6 cply class Poly
7 1 cv setvar s
8 7 6 cfv class Poly s
9 5 cv setvar p
10 4 cv setvar x
11 10 9 cfv class p x
12 cc0 class 0
13 11 12 wceq wff p x = 0
14 ccoe class coeff
15 9 14 cfv class coeff p
16 cdgr class deg
17 9 16 cfv class deg p
18 17 15 cfv class coeff p deg p
19 c1 class 1
20 18 19 wceq wff coeff p deg p = 1
21 13 20 wa wff p x = 0 coeff p deg p = 1
22 21 5 8 wrex wff p Poly s p x = 0 coeff p deg p = 1
23 22 4 2 crab class x | p Poly s p x = 0 coeff p deg p = 1
24 1 3 23 cmpt class s 𝒫 x | p Poly s p x = 0 coeff p deg p = 1
25 0 24 wceq wff IntgOver = s 𝒫 x | p Poly s p x = 0 coeff p deg p = 1