Metamath Proof Explorer

Theorem ditgsplitlem

Description: Lemma for ditgsplit . (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses ditgsplit.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
ditgsplit.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
ditgsplit.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
ditgsplit.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
ditgsplit.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 [,] 𝑌 ) )
ditgsplit.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐷 ∈ 𝑉 )
ditgsplit.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ 𝐿1 )
ditgsplit.1 ⊢ ( ( 𝜓 ∧ 𝜃 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) )
Assertion ditgsplitlem ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜃 ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ditgsplit.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 ditgsplit.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 ditgsplit.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
4 ditgsplit.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
5 ditgsplit.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 [,] 𝑌 ) )
6 ditgsplit.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐷 ∈ 𝑉 )
7 ditgsplit.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ 𝐿1 )
8 ditgsplit.1 ⊢ ( ( 𝜓 ∧ 𝜃 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) )
9 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) ) )
11 3 10 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌 ) )
12 11 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐴 ∈ ℝ )
14 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌 ) ) )
15 1 2 14 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌 ) ) )
16 5 15 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌 ) )
17 16 simp1d ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐶 ∈ ℝ )
19 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
20 1 2 19 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) ) )
21 4 20 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌 ) )
22 21 simp1d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐵 ∈ ℝ )
24 8 bilani ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) )
25 24 simpld ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐴 ≤ 𝐵 )
26 24 simprd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐵 ≤ 𝐶 )
27 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
28 12 17 27 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
30 23 25 26 29 mpbir3and ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
31 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
32 11 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐴 )
33 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐴 ) → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
34 31 32 33 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
35 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
36 16 simp3d ⊢ ( 𝜑 → 𝐶 ≤ 𝑌 )
37 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐶 ≤ 𝑌 ) → ( 𝑋 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
38 35 36 37 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
39 34 38 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
40 39 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
41 iblmbf ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ 𝐿1 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ MblFn )
42 7 41 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ MblFn )
43 42 6 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐷 ∈ ℂ )
44 40 43 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
46 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
47 31 32 46 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
48 21 simp3d ⊢ ( 𝜑 → 𝐵 ≤ 𝑌 )
49 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐵 ≤ 𝑌 ) → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
50 35 48 49 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
51 47 50 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
52 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
53 52 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
54 51 53 6 7 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
55 54 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
56 21 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
57 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
58 31 56 57 syl2anc ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
59 58 38 sstrd ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
60 ioombl ⊢ ( 𝐵 (,) 𝐶 ) ∈ dom vol
61 60 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ∈ dom vol )
62 59 61 6 7 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
64 13 18 30 45 55 63 itgsplitioo ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
65 13 23 18 25 26 letrd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐴 ≤ 𝐶 )
66 65 ditgpos ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 )
67 25 ditgpos ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 )
68 26 ditgpos ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
69 67 68 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
70 64 66 69 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) )
71 70 anassrs ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜃 ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) )