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