Definition df-ditg 26222

Description: Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The 𝐴 and 𝐵 here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use +∞, -∞ for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)

Assertion

Ref	Expression
df-ditg	⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)

Detailed syntax breakdown of Definition df-ditg

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4		cC	. . 3 class 𝐶
5	1, 2, 3, 4	cdit 26221	. 2 class ⨜[𝐴 → 𝐵]𝐶 d𝑥
6		cle 11383	. . . 4 class ≤
7	2, 3, 6	wbr 5108	. . 3 wff 𝐴 ≤ 𝐵
8		cioo 13516	. . . . 5 class (,)
9	2, 3, 8	co 7451	. . . 4 class (𝐴(,)𝐵)
10	1, 9, 4	citg 25994	. . 3 class ∫(𝐴(,)𝐵)𝐶 d𝑥
11	3, 2, 8	co 7451	. . . . 5 class (𝐵(,)𝐴)
12	1, 11, 4	citg 25994	. . . 4 class ∫(𝐵(,)𝐴)𝐶 d𝑥
13	12	cneg 11581	. . 3 class -∫(𝐵(,)𝐴)𝐶 d𝑥
14	7, 10, 13	cif 4485	. 2 class if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)
15	5, 14	wceq 1570	1 wff ⨜[𝐴 → 𝐵]𝐶 d𝑥 = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)

This definition is used by:  ditgeq1  26223  ditgeq2  26224  ditgeq3  26225  ditgex  26227  ditg0  26228  cbvditg  26229  ditgpos  26231  ditgneg  26232  ditgeq123i  37213  ditgeq123dv  37225  cbvditgvw2  37253  cbvditgdavw  37286  cbvditgdavw2  37302  ditgeq3d  47247