Definition df-ditg 23611

Description: Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The A and B 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 +oo , -oo for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)

Assertion

Ref	Expression
df-ditg	|- S__ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )

Detailed syntax breakdown of Definition df-ditg

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		cA	. . 3 class A
3		cB	. . 3 class B
4		cC	. . 3 class C
5	1, 2, 3, 4	cdit 23610	. 2 class S__ [ A -> B ] C _d x
6		cle 10075	. . . 4 class <_
7	2, 3, 6	wbr 4653	. . 3 wff A <_ B
8		cioo 12175	. . . . 5 class (,)
9	2, 3, 8	co 6650	. . . 4 class ( A (,) B )
10	1, 9, 4	citg 23387	. . 3 class S. ( A (,) B ) C _d x
11	3, 2, 8	co 6650	. . . . 5 class ( B (,) A )
12	1, 11, 4	citg 23387	. . . 4 class S. ( B (,) A ) C _d x
13	12	cneg 10267	. . 3 class -u S. ( B (,) A ) C _d x
14	7, 10, 13	cif 4086	. 2 class if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
15	5, 14	wceq 1483	1 wff S__ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )

This definition is referenced by:  ditgeq1  23612  ditgeq2  23613  ditgeq3  23614  ditgex  23616  ditg0  23617  cbvditg  23618  ditgpos  23620  ditgneg  23621  ditgeq3d  40180