This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgss2

Description: Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Assertion itgss2 
|- ( A C_ B -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
2 1 adantl 
 |-  ( ( A C_ B /\ x e. A ) -> if ( x e. A , C , 0 ) = C )
3 2 itgeq2dv 
 |-  ( A C_ B -> S. A if ( x e. A , C , 0 ) _d x = S. A C _d x )
4 id 
 |-  ( A C_ B -> A C_ B )
5 eldifn 
 |-  ( x e. ( B \ A ) -> -. x e. A )
6 5 iffalsed 
 |-  ( x e. ( B \ A ) -> if ( x e. A , C , 0 ) = 0 )
7 6 adantl 
 |-  ( ( A C_ B /\ x e. ( B \ A ) ) -> if ( x e. A , C , 0 ) = 0 )
8 4 7 itgss 
 |-  ( A C_ B -> S. A if ( x e. A , C , 0 ) _d x = S. B if ( x e. A , C , 0 ) _d x )
9 3 8 eqtr3d 
 |-  ( A C_ B -> S. A C _d x = S. B if ( x e. A , C , 0 ) _d x )