Theorem itgoval

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

	Ref	Expression
Assertion	itgoval	⊢ ( 𝑆 ⊆ ℂ → ( IntgOver ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2	1	elpw2	⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
3		fveq2	⊢ ( 𝑠 = 𝑆 → ( Poly ‘ 𝑠 ) = ( Poly ‘ 𝑆 ) )
4	3	rexeqdv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) ↔ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) ) )
5	4	rabbidv	⊢ ( 𝑠 = 𝑆 → { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )
6		df-itgo	⊢ IntgOver = ( 𝑠 ∈ 𝒫 ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑠 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )
7	1	rabex	⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } ∈ V
8	5 6 7	fvmpt	⊢ ( 𝑆 ∈ 𝒫 ℂ → ( IntgOver ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )
9	2 8	sylbir	⊢ ( 𝑆 ⊆ ℂ → ( IntgOver ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑝 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( deg ‘ 𝑝 ) ) = 1 ) } )