Theorem ditgeq3d

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

	Ref	Expression
Hypotheses	ditgeq3d.1	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ditgeq3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 = 𝐸 )
Assertion	ditgeq3d	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		ditgeq3d.1	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
2		ditgeq3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 = 𝐸 )
3		df-ditg	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 )
4	1	iftrued	⊢ ( 𝜑 → if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 ) = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 )
5	3 4	syl5eq	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 )
6	2	itgeq2dv	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 )
7		df-ditg	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 )
8	1	iftrued	⊢ ( 𝜑 → if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 ) = ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 )
9	7 8	eqtr2id	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 )
10	5 6 9	3eqtrd	⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 )