Metamath Proof Explorer

Theorem itgvallem3

Description: Lemma for itgposval and itgreval . (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis itgvallem3.1 
|- ( ( ph /\ x e. A ) -> B = 0 )
Assertion itgvallem3 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 itgvallem3.1 
 |-  ( ( ph /\ x e. A ) -> B = 0 )
2 1 adantrr 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ B ) ) -> B = 0 )
3 2 ifeq1da 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = if ( ( x e. A /\ 0 <_ B ) , 0 , 0 ) )
4 ifid 
 |-  if ( ( x e. A /\ 0 <_ B ) , 0 , 0 ) = 0
5 3 4 eqtrdi 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) = 0 )
6 5 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( x e. RR |-> 0 ) )
7 fconstmpt 
 |-  ( RR X. { 0 } ) = ( x e. RR |-> 0 )
8 6 7 eqtr4di 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) = ( RR X. { 0 } ) )
9 8 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) = ( S.2 ` ( RR X. { 0 } ) ) )
10 itg20 
 |-  ( S.2 ` ( RR X. { 0 } ) ) = 0
11 9 10 eqtrdi 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ B ) , B , 0 ) ) ) = 0 )