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	⊢ 𝐴 = 𝐵
	ditgeq123i.2	⊢ 𝐶 = 𝐷
	ditgeq123i.3	⊢ 𝐸 = 𝐹
Assertion	ditgeq123i	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑥

Proof

Step	Hyp	Ref	Expression
1		ditgeq123i.1	⊢ 𝐴 = 𝐵
2		ditgeq123i.2	⊢ 𝐶 = 𝐷
3		ditgeq123i.3	⊢ 𝐸 = 𝐹
4	1 2	breq12i	⊢ ( 𝐴 ≤ 𝐶 ↔ 𝐵 ≤ 𝐷 )
5	1 2	oveq12i	⊢ ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐷 )
6	5 3	itgeq12i	⊢ ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 = ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑥
7	2 1	oveq12i	⊢ ( 𝐶 (,) 𝐴 ) = ( 𝐷 (,) 𝐵 )
8	7 3	itgeq12i	⊢ ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥
9	8	negeqi	⊢ - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥
10	4 6 9	ifbieq12i	⊢ if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 ) = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑥 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥 )
11		df-ditg	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 )
12		df-ditg	⊢ ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑥 = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑥 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥 )
13	10 11 12	3eqtr4i	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑥