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 ( 𝐴 ⊆ 𝐵 → ∫ 𝐴 𝐶 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 𝑥 )