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

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 simpr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝜓 ∧ 𝜃 ) )
25 24 8 sylib ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) )
26 25 simpld ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐴 ≤ 𝐵 )
27 25 simprd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐵 ≤ 𝐶 )
28 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
29 12 17 28 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
31 23 26 27 30 mpbir3and ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
32 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
33 11 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐴 )
34 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐴 ) → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
35 32 33 34 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
36 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
37 16 simp3d ⊢ ( 𝜑 → 𝐶 ≤ 𝑌 )
38 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐶 ≤ 𝑌 ) → ( 𝑋 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
39 36 37 38 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
40 35 39 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
41 40 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
42 iblmbf ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ 𝐿1 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ MblFn )
43 7 42 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ MblFn )
44 43 6 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐷 ∈ ℂ )
45 41 44 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
47 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
48 32 33 47 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝐵 ) )
49 21 simp3d ⊢ ( 𝜑 → 𝐵 ≤ 𝑌 )
50 iooss2 ⊢ ( ( 𝑌 ∈ ℝ* ∧ 𝐵 ≤ 𝑌 ) → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
51 36 49 50 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
52 48 51 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝑋 (,) 𝑌 ) )
53 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
54 53 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
55 52 54 6 7 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
56 55 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
57 21 simp2d ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
58 iooss1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
59 32 57 58 syl2anc ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝐶 ) )
60 59 39 sstrd ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝑋 (,) 𝑌 ) )
61 ioombl ⊢ ( 𝐵 (,) 𝐶 ) ∈ dom vol
62 61 a1i ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ∈ dom vol )
63 60 62 6 7 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
64 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
65 13 18 31 46 56 64 itgsplitioo ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
66 13 23 18 26 27 letrd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → 𝐴 ≤ 𝐶 )
67 66 ditgpos ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 )
68 26 ditgpos ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 )
69 27 ditgpos ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
70 68 69 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
71 65 67 70 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜃 ) ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) )
72 71 anassrs ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜃 ) → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) )