Theorem ditgeq123i

Description: Equality inference for the directed integral. General version of ditgeq12i and ditgeq3i . (Contributed by GG, 1-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ditgeq123i.1	|- A = B
2		ditgeq123i.2	|- C = D
3		ditgeq123i.3	|- E = F
4	1 2	breq12i	|- ( A <_ C <-> B <_ D )
5	1 2	oveq12i	|- ( A (,) C ) = ( B (,) D )
6	5 3	itgeq12i	|- S. ( A (,) C ) E _d x = S. ( B (,) D ) F _d x
7	2 1	oveq12i	|- ( C (,) A ) = ( D (,) B )
8	7 3	itgeq12i	|- S. ( C (,) A ) E _d x = S. ( D (,) B ) F _d x
9	8	negeqi	|- -u S. ( C (,) A ) E _d x = -u S. ( D (,) B ) F _d x
10	4 6 9	ifbieq12i	|- 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	3eqtr4i	|- S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d x