Definition df-ditg

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3		vx	⊢ 𝑥
4	3 0 1 2	cdit	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥
5		cle	⊢ ≤
6	0 1 5	wbr	⊢ 𝐴 ≤ 𝐵
7		cioo	⊢ (,)
8	0 1 7	co	⊢ ( 𝐴 (,) 𝐵 )
9	3 8 2	citg	⊢ ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥
10	1 0 7	co	⊢ ( 𝐵 (,) 𝐴 )
11	3 10 2	citg	⊢ ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥
12	11	cneg	⊢ - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥
13	6 9 12	cif	⊢ if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
14	4 13	wceq	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )