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 C_ CC -> ( IntgOver ` S ) = { x e. CC | E. p e. ( Poly ` S ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 1 elpw2 
 |-  ( S e. ~P CC <-> S C_ CC )
3 fveq2 
 |-  ( s = S -> ( Poly ` s ) = ( Poly ` S ) )
4 3 rexeqdv 
 |-  ( s = S -> ( E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) <-> E. p e. ( Poly ` S ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) ) )
5 4 rabbidv 
 |-  ( s = S -> { x e. CC | E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } = { x e. CC | E. p e. ( Poly ` S ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )
6 df-itgo 
 |-  IntgOver = ( s e. ~P CC |-> { x e. CC | E. p e. ( Poly ` s ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )
7 1 rabex 
 |-  { x e. CC | E. p e. ( Poly ` S ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } e. _V
8 5 6 7 fvmpt 
 |-  ( S e. ~P CC -> ( IntgOver ` S ) = { x e. CC | E. p e. ( Poly ` S ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )
9 2 8 sylbir 
 |-  ( S C_ CC -> ( IntgOver ` S ) = { x e. CC | E. p e. ( Poly ` S ) ( ( p ` x ) = 0 /\ ( ( coeff ` p ) ` ( deg ` p ) ) = 1 ) } )