This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )