Metamath Proof Explorer

Theorem ditgeq3

Description: Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos first and use the equality theorems for df-itg .) (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditgeq3 
|- ( A. x e. RR D = E -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )

Proof

Step Hyp Ref Expression
1 ioossre 
 |-  ( A (,) B ) C_ RR
2 ssralv 
 |-  ( ( A (,) B ) C_ RR -> ( A. x e. RR D = E -> A. x e. ( A (,) B ) D = E ) )
3 1 2 ax-mp 
 |-  ( A. x e. RR D = E -> A. x e. ( A (,) B ) D = E )
4 itgeq2 
 |-  ( A. x e. ( A (,) B ) D = E -> S. ( A (,) B ) D _d x = S. ( A (,) B ) E _d x )
5 3 4 syl 
 |-  ( A. x e. RR D = E -> S. ( A (,) B ) D _d x = S. ( A (,) B ) E _d x )
6 ioossre 
 |-  ( B (,) A ) C_ RR
7 ssralv 
 |-  ( ( B (,) A ) C_ RR -> ( A. x e. RR D = E -> A. x e. ( B (,) A ) D = E ) )
8 6 7 ax-mp 
 |-  ( A. x e. RR D = E -> A. x e. ( B (,) A ) D = E )
9 itgeq2 
 |-  ( A. x e. ( B (,) A ) D = E -> S. ( B (,) A ) D _d x = S. ( B (,) A ) E _d x )
10 8 9 syl 
 |-  ( A. x e. RR D = E -> S. ( B (,) A ) D _d x = S. ( B (,) A ) E _d x )
11 10 negeqd 
 |-  ( A. x e. RR D = E -> -u S. ( B (,) A ) D _d x = -u S. ( B (,) A ) E _d x )
12 5 11 ifeq12d 
 |-  ( A. x e. RR D = E -> if ( A <_ B , S. ( A (,) B ) D _d x , -u S. ( B (,) A ) D _d x ) = if ( A <_ B , S. ( A (,) B ) E _d x , -u S. ( B (,) A ) E _d x ) )
13 df-ditg 
 |-  S_ [ A -> B ] D _d x = if ( A <_ B , S. ( A (,) B ) D _d x , -u S. ( B (,) A ) D _d x )
14 df-ditg 
 |-  S_ [ A -> B ] E _d x = if ( A <_ B , S. ( A (,) B ) E _d x , -u S. ( B (,) A ) E _d x )
15 12 13 14 3eqtr4g 
 |-  ( A. x e. RR D = E -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )