Theorem itgitg2

Description: Transfer an integral using S.2 to an equivalent integral using S. . (Contributed by Mario Carneiro, 6-Aug-2014)

	Ref	Expression
Hypotheses	itgitg2.1	$$⊢\left(\phi \wedge x\in ℝ\right)\to A\in ℝ$$
	itgitg2.2	$$⊢\left(\phi \wedge x\in ℝ\right)\to 0\le A$$
	itgitg2.3	$$⊢\phi \to \left(x\in ℝ⟼A\right)\in {𝐿}^1$$
Assertion	itgitg2	$$⊢\phi \to {\int }_{ℝ}Adx={\int }^2\left(\left(x\in ℝ⟼A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		itgitg2.1	$$⊢\left(\phi \wedge x\in ℝ\right)\to A\in ℝ$$
2		itgitg2.2	$$⊢\left(\phi \wedge x\in ℝ\right)\to 0\le A$$
3		itgitg2.3	$$⊢\phi \to \left(x\in ℝ⟼A\right)\in {𝐿}^1$$
4	1 3 2	itgposval	$$⊢\phi \to {\int }_{ℝ}Adx={\int }^2\left(\left(x\in ℝ⟼if\left(x\in ℝ,A,0\right)\right)\right)$$
5		iftrue	$$⊢x\in ℝ\to if\left(x\in ℝ,A,0\right)=A$$
6	5	mpteq2ia	$$⊢\left(x\in ℝ⟼if\left(x\in ℝ,A,0\right)\right)=\left(x\in ℝ⟼A\right)$$
7	6	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(x\in ℝ,A,0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼A\right)\right)$$
8	4 7	eqtrdi	$$⊢\phi \to {\int }_{ℝ}Adx={\int }^2\left(\left(x\in ℝ⟼A\right)\right)$$