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	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐷 ) ∈ 𝐿¹ )
	itgspliticc.6	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐷 ) ∈ 𝐿¹ )
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	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐷 ) ∈ 𝐿¹ )
6		itgspliticc.6	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ↦ 𝐷 ) ∈ 𝐿¹ )
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 𝑥 ) )

Metamath Proof Explorer

Theorem itgspliticc

Proof