ditgsplitlem

	Ref	Expression
Hypotheses	ditgsplit.x	$⊢ φ \to X \in ℝ$
	ditgsplit.y	$⊢ φ \to Y \in ℝ$
	ditgsplit.a	$⊢ φ \to A \in [X, Y]$
	ditgsplit.b	$⊢ φ \to B \in [X, Y]$
	ditgsplit.c	$⊢ φ \to C \in [X, Y]$
	ditgsplit.d	$⊢ (φ \land x \in (X, Y)) \to D \in V$
	ditgsplit.i	$⊢ φ \to (x \in (X, Y) ⟼ D) \in 𝐿^{1}$
	ditgsplit.1	$⊢ (ψ \land θ) \leftrightarrow (A \leq B \land B \leq C)$
Assertion	ditgsplitlem	$⊢ ((φ \land ψ) \land θ) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$

Proof

Step	Hyp	Ref	Expression
1		ditgsplit.x	$⊢ φ \to X \in ℝ$
2		ditgsplit.y	$⊢ φ \to Y \in ℝ$
3		ditgsplit.a	$⊢ φ \to A \in [X, Y]$
4		ditgsplit.b	$⊢ φ \to B \in [X, Y]$
5		ditgsplit.c	$⊢ φ \to C \in [X, Y]$
6		ditgsplit.d	$⊢ (φ \land x \in (X, Y)) \to D \in V$
7		ditgsplit.i	$⊢ φ \to (x \in (X, Y) ⟼ D) \in 𝐿^{1}$
8		ditgsplit.1	$⊢ (ψ \land θ) \leftrightarrow (A \leq B \land B \leq C)$
9		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
10	1 2 9	syl2anc	$⊢ φ \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
11	3 10	mpbid	$⊢ φ \to (A \in ℝ \land X \leq A \land A \leq Y)$
12	11	simp1d	$⊢ φ \to A \in ℝ$
13	12	adantr	$⊢ (φ \land (ψ \land θ)) \to A \in ℝ$
14		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (C \in [X, Y] \leftrightarrow (C \in ℝ \land X \leq C \land C \leq Y))$
15	1 2 14	syl2anc	$⊢ φ \to (C \in [X, Y] \leftrightarrow (C \in ℝ \land X \leq C \land C \leq Y))$
16	5 15	mpbid	$⊢ φ \to (C \in ℝ \land X \leq C \land C \leq Y)$
17	16	simp1d	$⊢ φ \to C \in ℝ$
18	17	adantr	$⊢ (φ \land (ψ \land θ)) \to C \in ℝ$
19		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
20	1 2 19	syl2anc	$⊢ φ \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
21	4 20	mpbid	$⊢ φ \to (B \in ℝ \land X \leq B \land B \leq Y)$
22	21	simp1d	$⊢ φ \to B \in ℝ$
23	22	adantr	$⊢ (φ \land (ψ \land θ)) \to B \in ℝ$
24	8	bilani	$⊢ (φ \land (ψ \land θ)) \to (A \leq B \land B \leq C)$
25	24	simpld	$⊢ (φ \land (ψ \land θ)) \to A \leq B$
26	24	simprd	$⊢ (φ \land (ψ \land θ)) \to B \leq C$
27		elicc2	$⊢ (A \in ℝ \land C \in ℝ) \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
28	12 17 27	syl2anc	$⊢ φ \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
29	28	adantr	$⊢ (φ \land (ψ \land θ)) \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
30	23 25 26 29	mpbir3and	$⊢ (φ \land (ψ \land θ)) \to B \in [A, C]$
31	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
32	11	simp2d	$⊢ φ \to X \leq A$
33		iooss1	$⊢ (X \in ℝ^{*} \land X \leq A) \to (A, C) \subseteq (X, C)$
34	31 32 33	syl2anc	$⊢ φ \to (A, C) \subseteq (X, C)$
35	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
36	16	simp3d	$⊢ φ \to C \leq Y$
37		iooss2	$⊢ (Y \in ℝ^{*} \land C \leq Y) \to (X, C) \subseteq (X, Y)$
38	35 36 37	syl2anc	$⊢ φ \to (X, C) \subseteq (X, Y)$
39	34 38	sstrd	$⊢ φ \to (A, C) \subseteq (X, Y)$
40	39	sselda	$⊢ (φ \land x \in (A, C)) \to x \in (X, Y)$
41		iblmbf	$⊢ (x \in (X, Y) ⟼ D) \in 𝐿^{1} \to (x \in (X, Y) ⟼ D) \in MblFn$
42	7 41	syl	$⊢ φ \to (x \in (X, Y) ⟼ D) \in MblFn$
43	42 6	mbfmptcl	$⊢ (φ \land x \in (X, Y)) \to D \in ℂ$
44	40 43	syldan	$⊢ (φ \land x \in (A, C)) \to D \in ℂ$
45	44	adantlr	$⊢ ((φ \land (ψ \land θ)) \land x \in (A, C)) \to D \in ℂ$
46		iooss1	$⊢ (X \in ℝ^{*} \land X \leq A) \to (A, B) \subseteq (X, B)$
47	31 32 46	syl2anc	$⊢ φ \to (A, B) \subseteq (X, B)$
48	21	simp3d	$⊢ φ \to B \leq Y$
49		iooss2	$⊢ (Y \in ℝ^{*} \land B \leq Y) \to (X, B) \subseteq (X, Y)$
50	35 48 49	syl2anc	$⊢ φ \to (X, B) \subseteq (X, Y)$
51	47 50	sstrd	$⊢ φ \to (A, B) \subseteq (X, Y)$
52		ioombl	$⊢ (A, B) \in dom vol$
53	52	a1i	$⊢ φ \to (A, B) \in dom vol$
54	51 53 6 7	iblss	$⊢ φ \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
55	54	adantr	$⊢ (φ \land (ψ \land θ)) \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
56	21	simp2d	$⊢ φ \to X \leq B$
57		iooss1	$⊢ (X \in ℝ^{*} \land X \leq B) \to (B, C) \subseteq (X, C)$
58	31 56 57	syl2anc	$⊢ φ \to (B, C) \subseteq (X, C)$
59	58 38	sstrd	$⊢ φ \to (B, C) \subseteq (X, Y)$
60		ioombl	$⊢ (B, C) \in dom vol$
61	60	a1i	$⊢ φ \to (B, C) \in dom vol$
62	59 61 6 7	iblss	$⊢ φ \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
63	62	adantr	$⊢ (φ \land (ψ \land θ)) \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
64	13 18 30 45 55 63	itgsplitioo	$⊢ (φ \land (ψ \land θ)) \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x$
65	13 23 18 25 26	letrd	$⊢ (φ \land (ψ \land θ)) \to A \leq C$
66	65	ditgpos	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{C} D d x = \int_{(A, C)} D d x$
67	25	ditgpos	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{B} D d x = \int_{(A, B)} D d x$
68	26	ditgpos	$⊢ (φ \land (ψ \land θ)) \to \int_{B}^{C} D d x = \int_{(B, C)} D d x$
69	67 68	oveq12d	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{B} D d x + \int_{B}^{C} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x$
70	64 66 69	3eqtr4d	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
71	70	anassrs	$⊢ ((φ \land ψ) \land θ) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$

Metamath Proof Explorer

Theorem ditgsplitlem

Proof