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 𝑥 )