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

Proof

Step	Hyp	Ref	Expression
1		ditgeq123dv.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		ditgeq123dv.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
3		ditgeq123dv.3	⊢ ( 𝜑 → 𝐸 = 𝐹 )
4	1 2	breq12d	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐶 ↔ 𝐵 ≤ 𝐷 ) )
5	1 2	oveq12d	⊢ ( 𝜑 → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐷 ) )
6	5 3	itgeq12sdv	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 = ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑥 )
7	2 1	oveq12d	⊢ ( 𝜑 → ( 𝐶 (,) 𝐴 ) = ( 𝐷 (,) 𝐵 ) )
8	7 3	itgeq12sdv	⊢ ( 𝜑 → ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥 )
9	8	negeqd	⊢ ( 𝜑 → - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 = - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥 )
10	4 6 9	ifbieq12d	⊢ ( 𝜑 → if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 ) = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑥 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥 ) )
11		df-ditg	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐸 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐸 d 𝑥 )
12		df-ditg	⊢ ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑥 = if ( 𝐵 ≤ 𝐷 , ∫ ( 𝐵 (,) 𝐷 ) 𝐹 d 𝑥 , - ∫ ( 𝐷 (,) 𝐵 ) 𝐹 d 𝑥 )
13	10 11 12	3eqtr4g	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐹 d 𝑥 )