Metamath Proof Explorer

Theorem ditgeqiooicc

Description: A function F on an open interval, has the same directed integral as its extension G on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ditgeqiooicc.1 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
ditgeqiooicc.2 
|- ( ph -> A e. RR )
ditgeqiooicc.3 
|- ( ph -> B e. RR )
ditgeqiooicc.4 
|- ( ph -> A <_ B )
ditgeqiooicc.5 
|- ( ph -> F : ( A (,) B ) --> RR )
Assertion ditgeqiooicc 
|- ( ph -> S_ [ A -> B ] ( F ` x ) _d x = S_ [ A -> B ] ( G ` x ) _d x )

Proof

Step Hyp Ref Expression
1 ditgeqiooicc.1 
 |-  G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
2 ditgeqiooicc.2 
 |-  ( ph -> A e. RR )
3 ditgeqiooicc.3 
 |-  ( ph -> B e. RR )
4 ditgeqiooicc.4 
 |-  ( ph -> A <_ B )
5 ditgeqiooicc.5 
 |-  ( ph -> F : ( A (,) B ) --> RR )
6 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
7 6 sseli 
 |-  ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
8 7 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
9 2 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR )
10 simpr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
11 9 rexrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR* )
12 3 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> B e. RR )
13 12 rexrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> B e. RR* )
14 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A (,) B ) <-> ( x e. RR /\ A < x /\ x < B ) ) )
15 11 13 14 syl2anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( x e. ( A (,) B ) <-> ( x e. RR /\ A < x /\ x < B ) ) )
16 10 15 mpbid 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( x e. RR /\ A < x /\ x < B ) )
17 16 simp2d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A < x )
18 9 17 gtned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
19 18 neneqd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
20 19 iffalsed 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
21 16 simp1d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR )
22 16 simp3d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x < B )
23 21 22 ltned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= B )
24 23 neneqd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x = B )
25 24 iffalsed 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
26 20 25 eqtrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
27 5 ffvelrnda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. RR )
28 26 27 eqeltrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. RR )
29 1 fvmpt2 
 |-  ( ( x e. ( A [,] B ) /\ if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. RR ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
30 8 28 29 syl2anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
31 30 20 25 3eqtrrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) = ( G ` x ) )
32 31 itgeq2dv 
 |-  ( ph -> S. ( A (,) B ) ( F ` x ) _d x = S. ( A (,) B ) ( G ` x ) _d x )
33 4 ditgpos 
 |-  ( ph -> S_ [ A -> B ] ( F ` x ) _d x = S. ( A (,) B ) ( F ` x ) _d x )
34 4 ditgpos 
 |-  ( ph -> S_ [ A -> B ] ( G ` x ) _d x = S. ( A (,) B ) ( G ` x ) _d x )
35 32 33 34 3eqtr4d 
 |-  ( ph -> S_ [ A -> B ] ( F ` x ) _d x = S_ [ A -> B ] ( G ` x ) _d x )