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 𝑥 )