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

Metamath Proof Explorer

Theorem itgspliticc

Description: The S. integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses itgspliticc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
itgspliticc.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
itgspliticc.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
itgspliticc.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ) → 𝐷 ∈ 𝑉 )
itgspliticc.5 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
itgspliticc.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
Assertion itgspliticc ( 𝜑 → ∫ ( 𝐴 [,] 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 [,] 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 [,] 𝐶 ) 𝐷 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgspliticc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 itgspliticc.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 itgspliticc.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
4 itgspliticc.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ) → 𝐷 ∈ 𝑉 )
5 itgspliticc.5 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
6 itgspliticc.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
7 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
8 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
9 1 2 8 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
10 3 9 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) )
11 10 simp1d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12 11 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
13 2 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
14 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
15 xrmaxle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ≤ 𝑧 ↔ ( 𝐴 ≤ 𝑧 ∧ 𝐵 ≤ 𝑧 ) ) )
16 xrlemin ⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑧 ≤ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝑧 ≤ 𝐵 ∧ 𝑧 ≤ 𝐶 ) ) )
17 14 15 16 ixxin ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ) → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) = ( if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) [,] if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) )
18 7 12 12 13 17 syl22anc ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) = ( if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) [,] if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) )
19 10 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
20 19 iftrued ⊢ ( 𝜑 → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
21 10 simp3d ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
22 21 iftrued ⊢ ( 𝜑 → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) = 𝐵 )
23 20 22 oveq12d ⊢ ( 𝜑 → ( if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) [,] if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) = ( 𝐵 [,] 𝐵 ) )
24 iccid ⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
25 12 24 syl ⊢ ( 𝜑 → ( 𝐵 [,] 𝐵 ) = { 𝐵 } )
26 18 23 25 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) = { 𝐵 } )
27 26 fveq2d ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) ) = ( vol* ‘ { 𝐵 } ) )
28 ovolsn ⊢ ( 𝐵 ∈ ℝ → ( vol* ‘ { 𝐵 } ) = 0 )
29 11 28 syl ⊢ ( 𝜑 → ( vol* ‘ { 𝐵 } ) = 0 )
30 27 29 eqtrd ⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐴 [,] 𝐵 ) ∩ ( 𝐵 [,] 𝐶 ) ) ) = 0 )
31 iccsplit ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ) → ( 𝐴 [,] 𝐶 ) = ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) )
32 1 2 3 31 syl3anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐶 ) = ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) )
33 30 32 4 5 6 itgsplit ⊢ ( 𝜑 → ∫ ( 𝐴 [,] 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 [,] 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 [,] 𝐶 ) 𝐷 d 𝑥 ) )