Metamath Proof Explorer

Theorem ditgswap

Description: Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses ditgcl.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
ditgcl.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
ditgcl.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
ditgcl.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
ditgcl.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ 𝑉 )
ditgcl.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ 𝐿1 )
Assertion ditgswap ( 𝜑 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 ditgcl.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 ditgcl.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 ditgcl.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
4 ditgcl.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
5 ditgcl.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ 𝑉 )
6 ditgcl.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ 𝐿1 )
7 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
9 3 8 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) )
10 9 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
13 4 12 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) )
14 13 simp1d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
15 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
16 10 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
17 14 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
18 15 16 17 ditgneg ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
19 15 ditgpos ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
20 19 negeqd ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → - ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = - ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 )
21 18 20 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 )
22 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
23 13 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
24 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐵 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝐴 ) )
25 22 23 24 syl2anc ⊢ ( 𝜑 → ( 𝐵 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝐴 ) )
26 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
27 9 simp3d ⊢ ( 𝜑 → 𝐴 ≤ 𝑌 )
28 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐴 ≤ 𝑌 ) → ( 𝑋 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝑌 ) )
29 26 27 28 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝑌 ) )
30 25 29 sstrd ⊢ ( 𝜑 → ( 𝐵 (,) 𝐴 ) ⊆ ( 𝑋 (,) 𝑌 ) )
31 30 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
32 iblmbf ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ MblFn )
33 6 32 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ MblFn )
34 33 5 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ ℂ )
35 31 34 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐴 ) ) → 𝐶 ∈ ℂ )
36 ioombl ⊢ ( 𝐵 (,) 𝐴 ) ∈ dom vol
37 36 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐴 ) ∈ dom vol )
38 30 37 5 6 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,) 𝐴 ) ↦ 𝐶 ) ∈ 𝐿1 )
39 35 38 itgcl ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ∈ ℂ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ∈ ℂ )
41 40 negnegd ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → - - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 = ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
42 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 )
43 14 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ∈ ℝ )
44 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
45 42 43 44 ditgneg ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
46 45 negeqd ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → - ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = - - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
47 42 ditgpos ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 )
48 41 46 47 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 )
49 10 14 21 48 lecasei ⊢ ( 𝜑 → ⨜ [ 𝐵 → 𝐴 ] 𝐶 d 𝑥 = - ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 )