Metamath Proof Explorer

Theorem itgoval

Description: Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion itgoval ⊢ S ⊆ ℂ → IntgOver ⁡ S = x ∈ ℂ | ∃ p ∈ Poly ⁡ S p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1

Proof

Step Hyp Ref Expression
1 cnex ⊢ ℂ ∈ V
2 1 elpw2 ⊢ S ∈ 𝒫 ℂ ↔ S ⊆ ℂ
3 fveq2 ⊢ s = S → Poly ⁡ s = Poly ⁡ S
4 3 rexeqdv ⊢ s = S → ∃ p ∈ Poly ⁡ s p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1 ↔ ∃ p ∈ Poly ⁡ S p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1
5 4 rabbidv ⊢ s = S → x ∈ ℂ | ∃ p ∈ Poly ⁡ s p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1 = x ∈ ℂ | ∃ p ∈ Poly ⁡ S p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1
6 df-itgo ⊢ IntgOver = s ∈ 𝒫 ℂ ⟼ x ∈ ℂ | ∃ p ∈ Poly ⁡ s p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1
7 1 rabex ⊢ x ∈ ℂ | ∃ p ∈ Poly ⁡ S p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1 ∈ V
8 5 6 7 fvmpt ⊢ S ∈ 𝒫 ℂ → IntgOver ⁡ S = x ∈ ℂ | ∃ p ∈ Poly ⁡ S p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1
9 2 8 sylbir ⊢ S ⊆ ℂ → IntgOver ⁡ S = x ∈ ℂ | ∃ p ∈ Poly ⁡ S p ⁡ x = 0 ∧ coeff ⁡ p ⁡ deg ⁡ p = 1