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 ABACdx=BifxAC0dx

Proof

Step Hyp Ref Expression
1 iftrue xAifxAC0=C
2 1 adantl ABxAifxAC0=C
3 2 itgeq2dv ABAifxAC0dx=ACdx
4 id ABAB
5 eldifn xBA¬xA
6 5 iffalsed xBAifxAC0=0
7 6 adantl ABxBAifxAC0=0
8 4 7 itgss ABAifxAC0dx=BifxAC0dx
9 3 8 eqtr3d ABACdx=BifxAC0dx