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⁡Sp⁡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⁡sp⁡x=0∧coeff⁡p⁡deg⁡p=1↔∃p∈Poly⁡Sp⁡x=0∧coeff⁡p⁡deg⁡p=1
5 4 rabbidv ⊢s=S→x∈ℂ|∃p∈Poly⁡sp⁡x=0∧coeff⁡p⁡deg⁡p=1=x∈ℂ|∃p∈Poly⁡Sp⁡x=0∧coeff⁡p⁡deg⁡p=1
6 df-itgo ⊢IntgOver=s∈𝒫ℂ⟼x∈ℂ|∃p∈Poly⁡sp⁡x=0∧coeff⁡p⁡deg⁡p=1
7 1 rabex ⊢x∈ℂ|∃p∈Poly⁡Sp⁡x=0∧coeff⁡p⁡deg⁡p=1∈V
8 5 6 7 fvmpt ⊢S∈𝒫ℂ→IntgOver⁡S=x∈ℂ|∃p∈Poly⁡Sp⁡x=0∧coeff⁡p⁡deg⁡p=1
9 2 8 sylbir ⊢S⊆ℂ→IntgOver⁡S=x∈ℂ|∃p∈Poly⁡Sp⁡x=0∧coeff⁡p⁡deg⁡p=1