Theorem ditgeq123dv

Description: Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	ditgeq123dv.1	|- ( ph -> A = B )
	ditgeq123dv.2	|- ( ph -> C = D )
	ditgeq123dv.3	|- ( ph -> E = F )
Assertion	ditgeq123dv	|- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d x )

Proof

Step	Hyp	Ref	Expression
1		ditgeq123dv.1	|- ( ph -> A = B )
2		ditgeq123dv.2	|- ( ph -> C = D )
3		ditgeq123dv.3	|- ( ph -> E = F )
4	1 2	breq12d	|- ( ph -> ( A <_ C <-> B <_ D ) )
5	1 2	oveq12d	|- ( ph -> ( A (,) C ) = ( B (,) D ) )
6	5 3	itgeq12sdv	|- ( ph -> S. ( A (,) C ) E _d x = S. ( B (,) D ) F _d x )
7	2 1	oveq12d	|- ( ph -> ( C (,) A ) = ( D (,) B ) )
8	7 3	itgeq12sdv	|- ( ph -> S. ( C (,) A ) E _d x = S. ( D (,) B ) F _d x )
9	8	negeqd	|- ( ph -> -u S. ( C (,) A ) E _d x = -u S. ( D (,) B ) F _d x )
10	4 6 9	ifbieq12d	|- ( ph -> if ( A <_ C , S. ( A (,) C ) E _d x , -u S. ( C (,) A ) E _d x ) = if ( B <_ D , S. ( B (,) D ) F _d x , -u S. ( D (,) B ) F _d x ) )
11		df-ditg	|- S_ [ A -> C ] E _d x = if ( A <_ C , S. ( A (,) C ) E _d x , -u S. ( C (,) A ) E _d x )
12		df-ditg	|- S_ [ B -> D ] F _d x = if ( B <_ D , S. ( B (,) D ) F _d x , -u S. ( D (,) B ) F _d x )
13	10 11 12	3eqtr4g	|- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d x )