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

Metamath Proof Explorer

Theorem ditgeq3

Description: Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos first and use the equality theorems for df-itg .) (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ditgeq3 ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 )

Proof

Step Hyp Ref Expression
1 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
2 ssralv ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐷 = 𝐸 ) )
3 1 2 ax-mp ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐷 = 𝐸 )
4 itgeq2 ⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) 𝐷 = 𝐸 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 )
5 3 4 syl ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 )
6 ioossre ⊢ ( 𝐵 (,) 𝐴 ) ⊆ ℝ
7 ssralv ⊢ ( ( 𝐵 (,) 𝐴 ) ⊆ ℝ → ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ∀ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) 𝐷 = 𝐸 ) )
8 6 7 ax-mp ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ∀ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) 𝐷 = 𝐸 )
9 itgeq2 ⊢ ( ∀ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) 𝐷 = 𝐸 → ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 )
10 8 9 syl ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 )
11 10 negeqd ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 = - ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 )
12 5 11 ifeq12d ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 ) = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 ) )
13 df-ditg ⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑥 )
14 df-ditg ⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐸 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐸 d 𝑥 )
15 12 13 14 3eqtr4g ⊢ ( ∀ 𝑥 ∈ ℝ 𝐷 = 𝐸 → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐸 d 𝑥 )