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

Proof

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

Metamath Proof Explorer

Theorem ditgeqiooicc

Proof