This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
ditgeqiooicc.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ditgeqiooicc.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ditgeqiooicc.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ditgeqiooicc.5 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
Assertion ditgeqiooicc ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐹 ‘ 𝑥 ) d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑥 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 ditgeqiooicc.1 ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
2 ditgeqiooicc.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ditgeqiooicc.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ditgeqiooicc.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ditgeqiooicc.5 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
6 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
7 6 sseli ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
11 9 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ )
13 12 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
14 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
15 11 13 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
16 10 15 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
17 16 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < 𝑥 )
18 9 17 gtned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 𝐴 )
19 18 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 𝐴 )
20 19 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
21 16 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℝ )
22 16 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 < 𝐵 )
23 21 22 ltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 𝐵 )
24 23 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 = 𝐵 )
25 24 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
26 20 25 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
27 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
28 26 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
29 1 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
30 8 28 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) = if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
31 30 20 25 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
32 31 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 )
33 4 ditgpos ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐹 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) d 𝑥 )
34 4 ditgpos ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑥 ) d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) ( 𝐺 ‘ 𝑥 ) d 𝑥 )
35 32 33 34 3eqtr4d ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] ( 𝐹 ‘ 𝑥 ) d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] ( 𝐺 ‘ 𝑥 ) d 𝑥 )