ditgswap

Description: Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	ditgcl.x	$⊢ φ \to X \in ℝ$
	ditgcl.y	$⊢ φ \to Y \in ℝ$
	ditgcl.a	$⊢ φ \to A \in [X, Y]$
	ditgcl.b	$⊢ φ \to B \in [X, Y]$
	ditgcl.c	$⊢ (φ \land x \in (X, Y)) \to C \in V$
	ditgcl.i	$⊢ φ \to (x \in (X, Y) ⟼ C) \in 𝐿^{1}$
Assertion	ditgswap	$⊢ φ \to \int_{B}^{A} C d x = - \int_{A}^{B} C d x$

Proof

Step	Hyp	Ref	Expression
1		ditgcl.x	$⊢ φ \to X \in ℝ$
2		ditgcl.y	$⊢ φ \to Y \in ℝ$
3		ditgcl.a	$⊢ φ \to A \in [X, Y]$
4		ditgcl.b	$⊢ φ \to B \in [X, Y]$
5		ditgcl.c	$⊢ (φ \land x \in (X, Y)) \to C \in V$
6		ditgcl.i	$⊢ φ \to (x \in (X, Y) ⟼ C) \in 𝐿^{1}$
7		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
8	1 2 7	syl2anc	$⊢ φ \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
9	3 8	mpbid	$⊢ φ \to (A \in ℝ \land X \leq A \land A \leq Y)$
10	9	simp1d	$⊢ φ \to A \in ℝ$
11		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
12	1 2 11	syl2anc	$⊢ φ \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
13	4 12	mpbid	$⊢ φ \to (B \in ℝ \land X \leq B \land B \leq Y)$
14	13	simp1d	$⊢ φ \to B \in ℝ$
15		simpr	$⊢ (φ \land A \leq B) \to A \leq B$
16	10	adantr	$⊢ (φ \land A \leq B) \to A \in ℝ$
17	14	adantr	$⊢ (φ \land A \leq B) \to B \in ℝ$
18	15 16 17	ditgneg	$⊢ (φ \land A \leq B) \to \int_{B}^{A} C d x = - \int_{(A, B)} C d x$
19	15	ditgpos	$⊢ (φ \land A \leq B) \to \int_{A}^{B} C d x = \int_{(A, B)} C d x$
20	19	negeqd	$⊢ (φ \land A \leq B) \to - \int_{A}^{B} C d x = - \int_{(A, B)} C d x$
21	18 20	eqtr4d	$⊢ (φ \land A \leq B) \to \int_{B}^{A} C d x = - \int_{A}^{B} C d x$
22	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
23	13	simp2d	$⊢ φ \to X \leq B$
24		iooss1	$⊢ (X \in ℝ^{*} \land X \leq B) \to (B, A) \subseteq (X, A)$
25	22 23 24	syl2anc	$⊢ φ \to (B, A) \subseteq (X, A)$
26	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
27	9	simp3d	$⊢ φ \to A \leq Y$
28		iooss2	$⊢ (Y \in ℝ^{*} \land A \leq Y) \to (X, A) \subseteq (X, Y)$
29	26 27 28	syl2anc	$⊢ φ \to (X, A) \subseteq (X, Y)$
30	25 29	sstrd	$⊢ φ \to (B, A) \subseteq (X, Y)$
31	30	sselda	$⊢ (φ \land x \in (B, A)) \to x \in (X, Y)$
32		iblmbf	$⊢ (x \in (X, Y) ⟼ C) \in 𝐿^{1} \to (x \in (X, Y) ⟼ C) \in MblFn$
33	6 32	syl	$⊢ φ \to (x \in (X, Y) ⟼ C) \in MblFn$
34	33 5	mbfmptcl	$⊢ (φ \land x \in (X, Y)) \to C \in ℂ$
35	31 34	syldan	$⊢ (φ \land x \in (B, A)) \to C \in ℂ$
36		ioombl	$⊢ (B, A) \in dom vol$
37	36	a1i	$⊢ φ \to (B, A) \in dom vol$
38	30 37 5 6	iblss	$⊢ φ \to (x \in (B, A) ⟼ C) \in 𝐿^{1}$
39	35 38	itgcl	$⊢ φ \to \int_{(B, A)} C d x \in ℂ$
40	39	adantr	$⊢ (φ \land B \leq A) \to \int_{(B, A)} C d x \in ℂ$
41	40	negnegd	$⊢ (φ \land B \leq A) \to - (- \int_{(B, A)} C d x) = \int_{(B, A)} C d x$
42		simpr	$⊢ (φ \land B \leq A) \to B \leq A$
43	14	adantr	$⊢ (φ \land B \leq A) \to B \in ℝ$
44	10	adantr	$⊢ (φ \land B \leq A) \to A \in ℝ$
45	42 43 44	ditgneg	$⊢ (φ \land B \leq A) \to \int_{A}^{B} C d x = - \int_{(B, A)} C d x$
46	45	negeqd	$⊢ (φ \land B \leq A) \to - \int_{A}^{B} C d x = - (- \int_{(B, A)} C d x)$
47	42	ditgpos	$⊢ (φ \land B \leq A) \to \int_{B}^{A} C d x = \int_{(B, A)} C d x$
48	41 46 47	3eqtr4rd	$⊢ (φ \land B \leq A) \to \int_{B}^{A} C d x = - \int_{A}^{B} C d x$
49	10 14 21 48	lecasei	$⊢ φ \to \int_{B}^{A} C d x = - \int_{A}^{B} C d x$

Metamath Proof Explorer

Theorem ditgswap

Proof