Theorem ditgeq3d

Description: Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ditgeq3d.1	|- ( ph -> A <_ B )
	ditgeq3d.2	|- ( ( ph /\ x e. ( A (,) B ) ) -> D = E )
Assertion	ditgeq3d	|- ( ph -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )

Proof

Step	Hyp	Ref	Expression
1		ditgeq3d.1	|- ( ph -> A <_ B )
2		ditgeq3d.2	|- ( ( ph /\ x e. ( A (,) B ) ) -> D = E )
3		df-ditg	|- S_ [ A -> B ] D _d x = if ( A <_ B , S. ( A (,) B ) D _d x , -u S. ( B (,) A ) D _d x )
4	1	iftrued	|- ( ph -> if ( A <_ B , S. ( A (,) B ) D _d x , -u S. ( B (,) A ) D _d x ) = S. ( A (,) B ) D _d x )
5	3 4	syl5eq	|- ( ph -> S_ [ A -> B ] D _d x = S. ( A (,) B ) D _d x )
6	2	itgeq2dv	|- ( ph -> S. ( A (,) B ) D _d x = S. ( A (,) B ) E _d x )
7		df-ditg	|- S_ [ A -> B ] E _d x = if ( A <_ B , S. ( A (,) B ) E _d x , -u S. ( B (,) A ) E _d x )
8	1	iftrued	|- ( ph -> if ( A <_ B , S. ( A (,) B ) E _d x , -u S. ( B (,) A ) E _d x ) = S. ( A (,) B ) E _d x )
9	7 8	syl5req	|- ( ph -> S. ( A (,) B ) E _d x = S_ [ A -> B ] E _d x )
10	5 6 9	3eqtrd	|- ( ph -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )