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\subseteq B\to {\int }_{A}Cdx={\int }_{B}if\left(x\in A,C,0\right)dx$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢x\in A\to if\left(x\in A,C,0\right)=C$$
2	1	adantl	$$⊢\left(A\subseteq B\wedge x\in A\right)\to if\left(x\in A,C,0\right)=C$$
3	2	itgeq2dv	$$⊢A\subseteq B\to {\int }_{A}if\left(x\in A,C,0\right)dx={\int }_{A}Cdx$$
4		id	$$⊢A\subseteq B\to A\subseteq B$$
5		eldifn	$$⊢x\in \left(B\setminus A\right)\to \neg x\in A$$
6	5	iffalsed	$$⊢x\in \left(B\setminus A\right)\to if\left(x\in A,C,0\right)=0$$
7	6	adantl	$$⊢\left(A\subseteq B\wedge x\in \left(B\setminus A\right)\right)\to if\left(x\in A,C,0\right)=0$$
8	4 7	itgss	$$⊢A\subseteq B\to {\int }_{A}if\left(x\in A,C,0\right)dx={\int }_{B}if\left(x\in A,C,0\right)dx$$
9	3 8	eqtr3d	$$⊢A\subseteq B\to {\int }_{A}Cdx={\int }_{B}if\left(x\in A,C,0\right)dx$$