Theorem ditgpos

Description: Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypothesis	ditgpos.1	|- ( ph -> A <_ B )
Assertion	ditgpos	|- ( ph -> S_ [ A -> B ] C _d x = S. ( A (,) B ) C _d x )

Proof

Step	Hyp	Ref	Expression
1		ditgpos.1	|- ( ph -> A <_ B )
2		df-ditg	|- S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
3	1	iftrued	|- ( ph -> if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) = S. ( A (,) B ) C _d x )
4	2 3	syl5eq	|- ( ph -> S_ [ A -> B ] C _d x = S. ( A (,) B ) C _d x )