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	|- ( ( ph /\ x e. RR ) -> A e. RR )
	itgitg2.2	|- ( ( ph /\ x e. RR ) -> 0 <_ A )
	itgitg2.3	|- ( ph -> ( x e. RR |-> A ) e. L^1 )
Assertion	itgitg2	|- ( ph -> S. RR A _d x = ( S.2 ` ( x e. RR |-> A ) ) )

Proof

Step	Hyp	Ref	Expression
1		itgitg2.1	|- ( ( ph /\ x e. RR ) -> A e. RR )
2		itgitg2.2	|- ( ( ph /\ x e. RR ) -> 0 <_ A )
3		itgitg2.3	|- ( ph -> ( x e. RR |-> A ) e. L^1 )
4	1 3 2	itgposval	|- ( ph -> S. RR A _d x = ( S.2 ` ( x e. RR |-> if ( x e. RR , A , 0 ) ) ) )
5		iftrue	|- ( x e. RR -> if ( x e. RR , A , 0 ) = A )
6	5	mpteq2ia	|- ( x e. RR |-> if ( x e. RR , A , 0 ) ) = ( x e. RR |-> A )
7	6	fveq2i	|- ( S.2 ` ( x e. RR |-> if ( x e. RR , A , 0 ) ) ) = ( S.2 ` ( x e. RR |-> A ) )
8	4 7	eqtrdi	|- ( ph -> S. RR A _d x = ( S.2 ` ( x e. RR |-> A ) ) )