# 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}=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\right)$
ditgeqiooicc.2 ${⊢}{\phi }\to {A}\in ℝ$
ditgeqiooicc.3 ${⊢}{\phi }\to {B}\in ℝ$
ditgeqiooicc.4 ${⊢}{\phi }\to {A}\le {B}$
ditgeqiooicc.5 ${⊢}{\phi }\to {F}:\left({A},{B}\right)⟶ℝ$
Assertion ditgeqiooicc ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{F}\left({x}\right)d{x}={\int }_{{A}}^{{B}}{G}\left({x}\right)d{x}$

### Proof

Step Hyp Ref Expression
1 ditgeqiooicc.1 ${⊢}{G}=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\right)$
2 ditgeqiooicc.2 ${⊢}{\phi }\to {A}\in ℝ$
3 ditgeqiooicc.3 ${⊢}{\phi }\to {B}\in ℝ$
4 ditgeqiooicc.4 ${⊢}{\phi }\to {A}\le {B}$
5 ditgeqiooicc.5 ${⊢}{\phi }\to {F}:\left({A},{B}\right)⟶ℝ$
6 ioossicc ${⊢}\left({A},{B}\right)\subseteq \left[{A},{B}\right]$
7 6 sseli ${⊢}{x}\in \left({A},{B}\right)\to {x}\in \left[{A},{B}\right]$
8 7 adantl ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\in \left[{A},{B}\right]$
9 2 adantr ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {A}\in ℝ$
10 simpr ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\in \left({A},{B}\right)$
11 9 rexrd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {A}\in {ℝ}^{*}$
12 3 adantr ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {B}\in ℝ$
13 12 rexrd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {B}\in {ℝ}^{*}$
14 elioo2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({x}\in \left({A},{B}\right)↔\left({x}\in ℝ\wedge {A}<{x}\wedge {x}<{B}\right)\right)$
15 11 13 14 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to \left({x}\in \left({A},{B}\right)↔\left({x}\in ℝ\wedge {A}<{x}\wedge {x}<{B}\right)\right)$
16 10 15 mpbid ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to \left({x}\in ℝ\wedge {A}<{x}\wedge {x}<{B}\right)$
17 16 simp2d ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {A}<{x}$
18 9 17 gtned ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\ne {A}$
19 18 neneqd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to ¬{x}={A}$
20 19 iffalsed ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={B},{L},{F}\left({x}\right)\right)$
21 16 simp1d ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\in ℝ$
22 16 simp3d ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}<{B}$
23 21 22 ltned ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\ne {B}$
24 23 neneqd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to ¬{x}={B}$
25 24 iffalsed ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to if\left({x}={B},{L},{F}\left({x}\right)\right)={F}\left({x}\right)$
26 20 25 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={F}\left({x}\right)$
27 5 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {F}\left({x}\right)\in ℝ$
28 26 27 eqeltrd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℝ$
29 1 fvmpt2 ${⊢}\left({x}\in \left[{A},{B}\right]\wedge if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℝ\right)\to {G}\left({x}\right)=if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)$
30 8 28 29 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {G}\left({x}\right)=if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)$
31 30 20 25 3eqtrrd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {F}\left({x}\right)={G}\left({x}\right)$
32 31 itgeq2dv ${⊢}{\phi }\to {\int }_{\left({A},{B}\right)}{F}\left({x}\right)d{x}={\int }_{\left({A},{B}\right)}{G}\left({x}\right)d{x}$
33 4 ditgpos ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{F}\left({x}\right)d{x}={\int }_{\left({A},{B}\right)}{F}\left({x}\right)d{x}$
34 4 ditgpos ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{G}\left({x}\right)d{x}={\int }_{\left({A},{B}\right)}{G}\left({x}\right)d{x}$
35 32 33 34 3eqtr4d ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{F}\left({x}\right)d{x}={\int }_{{A}}^{{B}}{G}\left({x}\right)d{x}$