This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → ⨜ [ 𝐴 → 𝐵 ] 𝐷 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 𝑥 )