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