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 )