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	⊢ ( 𝐴 ⊆ 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		iftrue	⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
2	1	adantl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
3	2	itgeq2dv	⊢ ( 𝐴 ⊆ 𝐵 → ∫ 𝐴 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 = ∫ 𝐴 𝐶 d 𝑥 )
4		id	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 )
5		eldifn	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
6	5	iffalsed	⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
7	6	adantl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
8	4 7	itgss	⊢ ( 𝐴 ⊆ 𝐵 → ∫ 𝐴 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 = ∫ 𝐵 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 )
9	3 8	eqtr3d	⊢ ( 𝐴 ⊆ 𝐵 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 if ( 𝑥 ∈ 𝐴 , 𝐶 , 0 ) d 𝑥 )