Metamath Proof Explorer

Theorem iblposlem

Description: Lemma for iblpos . (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblrelem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
iblpos.2 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion iblposlem 
|- ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 iblrelem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 iblpos.2 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
3 1 le0neg2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ B <-> -u B <_ 0 ) )
4 2 3 mpbid 
 |-  ( ( ph /\ x e. A ) -> -u B <_ 0 )
5 4 adantrr 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B <_ 0 )
6 simprr 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> 0 <_ -u B )
7 1 adantrr 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> B e. RR )
8 7 renegcld 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B e. RR )
9 0re 
 |-  0 e. RR
10 letri3 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> ( -u B = 0 <-> ( -u B <_ 0 /\ 0 <_ -u B ) ) )
11 8 9 10 sylancl 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> ( -u B = 0 <-> ( -u B <_ 0 /\ 0 <_ -u B ) ) )
12 5 6 11 mpbir2and 
 |-  ( ( ph /\ ( x e. A /\ 0 <_ -u B ) ) -> -u B = 0 )
13 12 ifeq1da 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = if ( ( x e. A /\ 0 <_ -u B ) , 0 , 0 ) )
14 ifid 
 |-  if ( ( x e. A /\ 0 <_ -u B ) , 0 , 0 ) = 0
15 13 14 eqtrdi 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) = 0 )
16 15 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) = ( x e. RR |-> 0 ) )
17 fconstmpt 
 |-  ( RR X. { 0 } ) = ( x e. RR |-> 0 )
18 16 17 eqtr4di 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) = ( RR X. { 0 } ) )
19 18 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = ( S.2 ` ( RR X. { 0 } ) ) )
20 itg20 
 |-  ( S.2 ` ( RR X. { 0 } ) ) = 0
21 19 20 eqtrdi 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u B ) , -u B , 0 ) ) ) = 0 )