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		simpr	$⊢ (φ \land (ψ \land θ)) \to (ψ \land θ)$
25	24 8	sylib	$⊢ (φ \land (ψ \land θ)) \to (A \leq B \land B \leq C)$
26	25	simpld	$⊢ (φ \land (ψ \land θ)) \to A \leq B$
27	25	simprd	$⊢ (φ \land (ψ \land θ)) \to B \leq C$
28		elicc2	$⊢ (A \in ℝ \land C \in ℝ) \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
29	12 17 28	syl2anc	$⊢ φ \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
30	29	adantr	$⊢ (φ \land (ψ \land θ)) \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
31	23 26 27 30	mpbir3and	$⊢ (φ \land (ψ \land θ)) \to B \in [A, C]$
32	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
33	11	simp2d	$⊢ φ \to X \leq A$
34		iooss1	$⊢ (X \in ℝ^{*} \land X \leq A) \to (A, C) \subseteq (X, C)$
35	32 33 34	syl2anc	$⊢ φ \to (A, C) \subseteq (X, C)$
36	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
37	16	simp3d	$⊢ φ \to C \leq Y$
38		iooss2	$⊢ (Y \in ℝ^{*} \land C \leq Y) \to (X, C) \subseteq (X, Y)$
39	36 37 38	syl2anc	$⊢ φ \to (X, C) \subseteq (X, Y)$
40	35 39	sstrd	$⊢ φ \to (A, C) \subseteq (X, Y)$
41	40	sselda	$⊢ (φ \land x \in (A, C)) \to x \in (X, Y)$
42		iblmbf	$⊢ (x \in (X, Y) ⟼ D) \in 𝐿^{1} \to (x \in (X, Y) ⟼ D) \in MblFn$
43	7 42	syl	$⊢ φ \to (x \in (X, Y) ⟼ D) \in MblFn$
44	43 6	mbfmptcl	$⊢ (φ \land x \in (X, Y)) \to D \in ℂ$
45	41 44	syldan	$⊢ (φ \land x \in (A, C)) \to D \in ℂ$
46	45	adantlr	$⊢ ((φ \land (ψ \land θ)) \land x \in (A, C)) \to D \in ℂ$
47		iooss1	$⊢ (X \in ℝ^{*} \land X \leq A) \to (A, B) \subseteq (X, B)$
48	32 33 47	syl2anc	$⊢ φ \to (A, B) \subseteq (X, B)$
49	21	simp3d	$⊢ φ \to B \leq Y$
50		iooss2	$⊢ (Y \in ℝ^{*} \land B \leq Y) \to (X, B) \subseteq (X, Y)$
51	36 49 50	syl2anc	$⊢ φ \to (X, B) \subseteq (X, Y)$
52	48 51	sstrd	$⊢ φ \to (A, B) \subseteq (X, Y)$
53		ioombl	$⊢ (A, B) \in dom vol$
54	53	a1i	$⊢ φ \to (A, B) \in dom vol$
55	52 54 6 7	iblss	$⊢ φ \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
56	55	adantr	$⊢ (φ \land (ψ \land θ)) \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
57	21	simp2d	$⊢ φ \to X \leq B$
58		iooss1	$⊢ (X \in ℝ^{*} \land X \leq B) \to (B, C) \subseteq (X, C)$
59	32 57 58	syl2anc	$⊢ φ \to (B, C) \subseteq (X, C)$
60	59 39	sstrd	$⊢ φ \to (B, C) \subseteq (X, Y)$
61		ioombl	$⊢ (B, C) \in dom vol$
62	61	a1i	$⊢ φ \to (B, C) \in dom vol$
63	60 62 6 7	iblss	$⊢ φ \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
64	63	adantr	$⊢ (φ \land (ψ \land θ)) \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
65	13 18 31 46 56 64	itgsplitioo	$⊢ (φ \land (ψ \land θ)) \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x$
66	13 23 18 26 27	letrd	$⊢ (φ \land (ψ \land θ)) \to A \leq C$
67	66	ditgpos	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{C} D d x = \int_{(A, C)} D d x$
68	26	ditgpos	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{B} D d x = \int_{(A, B)} D d x$
69	27	ditgpos	$⊢ (φ \land (ψ \land θ)) \to \int_{B}^{C} D d x = \int_{(B, C)} D d x$
70	68 69	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$
71	65 67 70	3eqtr4d	$⊢ (φ \land (ψ \land θ)) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
72	71	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