ditgsplit

Description: This theorem is the raison d'être for the directed integral, because unlike itgspliticc , there is no constraint on the ordering of the points A , B , C in the domain. (Contributed by Mario Carneiro, 13-Aug-2014)

	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}$
Assertion	ditgsplit	$⊢ φ \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		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
9	1 2 8	syl2anc	$⊢ φ \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
10	3 9	mpbid	$⊢ φ \to (A \in ℝ \land X \leq A \land A \leq Y)$
11	10	simp1d	$⊢ φ \to A \in ℝ$
12		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
13	1 2 12	syl2anc	$⊢ φ \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
14	4 13	mpbid	$⊢ φ \to (B \in ℝ \land X \leq B \land B \leq Y)$
15	14	simp1d	$⊢ φ \to B \in ℝ$
16	11	adantr	$⊢ (φ \land A \leq B) \to A \in ℝ$
17		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (C \in [X, Y] \leftrightarrow (C \in ℝ \land X \leq C \land C \leq Y))$
18	1 2 17	syl2anc	$⊢ φ \to (C \in [X, Y] \leftrightarrow (C \in ℝ \land X \leq C \land C \leq Y))$
19	5 18	mpbid	$⊢ φ \to (C \in ℝ \land X \leq C \land C \leq Y)$
20	19	simp1d	$⊢ φ \to C \in ℝ$
21	20	adantr	$⊢ (φ \land A \leq B) \to C \in ℝ$
22	15	ad2antrr	$⊢ ((φ \land A \leq B) \land A \leq C) \to B \in ℝ$
23	20	ad2antrr	$⊢ ((φ \land A \leq B) \land A \leq C) \to C \in ℝ$
24		biid	$⊢ (A \leq B \land B \leq C) \leftrightarrow (A \leq B \land B \leq C)$
25	1 2 3 4 5 6 7 24	ditgsplitlem	$⊢ ((φ \land A \leq B) \land B \leq C) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
26	25	adantlr	$⊢ (((φ \land A \leq B) \land A \leq C) \land B \leq C) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
27		biid	$⊢ (A \leq C \land C \leq B) \leftrightarrow (A \leq C \land C \leq B)$
28	1 2 3 5 4 6 7 27	ditgsplitlem	$⊢ ((φ \land A \leq C) \land C \leq B) \to \int_{A}^{B} D d x = \int_{A}^{C} D d x + \int_{C}^{B} D d x$
29	28	oveq1d	$⊢ ((φ \land A \leq C) \land C \leq B) \to \int_{A}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x$
30	1 2 3 5 6 7	ditgcl	$⊢ φ \to \int_{A}^{C} D d x \in ℂ$
31	1 2 5 4 6 7	ditgcl	$⊢ φ \to \int_{C}^{B} D d x \in ℂ$
32	1 2 4 5 6 7	ditgcl	$⊢ φ \to \int_{B}^{C} D d x \in ℂ$
33	30 31 32	addassd	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x$
34	1 2 5 4 6 7	ditgswap	$⊢ φ \to \int_{B}^{C} D d x = - \int_{C}^{B} D d x$
35	34	oveq2d	$⊢ φ \to \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{C}^{B} D d x + (- \int_{C}^{B} D d x)$
36	31	negidd	$⊢ φ \to \int_{C}^{B} D d x + (- \int_{C}^{B} D d x) = 0$
37	35 36	eqtrd	$⊢ φ \to \int_{C}^{B} D d x + \int_{B}^{C} D d x = 0$
38	37	oveq2d	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x + 0$
39	30	addridd	$⊢ φ \to \int_{A}^{C} D d x + 0 = \int_{A}^{C} D d x$
40	33 38 39	3eqtrd	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x$
41	40	ad2antrr	$⊢ ((φ \land A \leq C) \land C \leq B) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x$
42	29 41	eqtr2d	$⊢ ((φ \land A \leq C) \land C \leq B) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
43	42	adantllr	$⊢ (((φ \land A \leq B) \land A \leq C) \land C \leq B) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
44	22 23 26 43	lecasei	$⊢ ((φ \land A \leq B) \land A \leq C) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
45	40	ad2antrr	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x$
46		ancom	$⊢ (A \leq B \land C \leq A) \leftrightarrow (C \leq A \land A \leq B)$
47	1 2 5 3 4 6 7 46	ditgsplitlem	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{C}^{B} D d x = \int_{C}^{A} D d x + \int_{A}^{B} D d x$
48	47	oveq2d	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x = \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x$
49	1 2 3 5 6 7	ditgswap	$⊢ φ \to \int_{C}^{A} D d x = - \int_{A}^{C} D d x$
50	49	oveq2d	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{A} D d x = \int_{A}^{C} D d x + (- \int_{A}^{C} D d x)$
51	30	negidd	$⊢ φ \to \int_{A}^{C} D d x + (- \int_{A}^{C} D d x) = 0$
52	50 51	eqtrd	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{A} D d x = 0$
53	52	oveq1d	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x = 0 + \int_{A}^{B} D d x$
54	1 2 5 3 6 7	ditgcl	$⊢ φ \to \int_{C}^{A} D d x \in ℂ$
55	1 2 3 4 6 7	ditgcl	$⊢ φ \to \int_{A}^{B} D d x \in ℂ$
56	30 54 55	addassd	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x = \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x$
57	55	addlidd	$⊢ φ \to 0 + \int_{A}^{B} D d x = \int_{A}^{B} D d x$
58	53 56 57	3eqtr3d	$⊢ φ \to \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x = \int_{A}^{B} D d x$
59	58	ad2antrr	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x = \int_{A}^{B} D d x$
60	48 59	eqtrd	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x = \int_{A}^{B} D d x$
61	60	oveq1d	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
62	45 61	eqtr3d	$⊢ ((φ \land A \leq B) \land C \leq A) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
63	16 21 44 62	lecasei	$⊢ (φ \land A \leq B) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
64	11	adantr	$⊢ (φ \land B \leq A) \to A \in ℝ$
65	20	adantr	$⊢ (φ \land B \leq A) \to C \in ℝ$
66		biid	$⊢ (B \leq A \land A \leq C) \leftrightarrow (B \leq A \land A \leq C)$
67	1 2 4 3 5 6 7 66	ditgsplitlem	$⊢ ((φ \land B \leq A) \land A \leq C) \to \int_{B}^{C} D d x = \int_{B}^{A} D d x + \int_{A}^{C} D d x$
68	67	oveq2d	$⊢ ((φ \land B \leq A) \land A \leq C) \to \int_{A}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x$
69	1 2 3 4 6 7	ditgswap	$⊢ φ \to \int_{B}^{A} D d x = - \int_{A}^{B} D d x$
70	69	oveq2d	$⊢ φ \to \int_{A}^{B} D d x + \int_{B}^{A} D d x = \int_{A}^{B} D d x + (- \int_{A}^{B} D d x)$
71	55	negidd	$⊢ φ \to \int_{A}^{B} D d x + (- \int_{A}^{B} D d x) = 0$
72	70 71	eqtrd	$⊢ φ \to \int_{A}^{B} D d x + \int_{B}^{A} D d x = 0$
73	72	oveq1d	$⊢ φ \to \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x = 0 + \int_{A}^{C} D d x$
74	1 2 4 3 6 7	ditgcl	$⊢ φ \to \int_{B}^{A} D d x \in ℂ$
75	55 74 30	addassd	$⊢ φ \to \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x$
76	30	addlidd	$⊢ φ \to 0 + \int_{A}^{C} D d x = \int_{A}^{C} D d x$
77	73 75 76	3eqtr3d	$⊢ φ \to \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x = \int_{A}^{C} D d x$
78	77	ad2antrr	$⊢ ((φ \land B \leq A) \land A \leq C) \to \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x = \int_{A}^{C} D d x$
79	68 78	eqtr2d	$⊢ ((φ \land B \leq A) \land A \leq C) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
80	15	ad2antrr	$⊢ ((φ \land B \leq A) \land C \leq A) \to B \in ℝ$
81	20	ad2antrr	$⊢ ((φ \land B \leq A) \land C \leq A) \to C \in ℝ$
82		ancom	$⊢ (C \leq A \land B \leq C) \leftrightarrow (B \leq C \land C \leq A)$
83	1 2 4 5 3 6 7 82	ditgsplitlem	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{B}^{A} D d x = \int_{B}^{C} D d x + \int_{C}^{A} D d x$
84	83	oveq1d	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{B}^{A} D d x + \int_{A}^{C} D d x = \int_{B}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{C} D d x$
85	32 54 30	addassd	$⊢ φ \to \int_{B}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{C} D d x = \int_{B}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{C} D d x$
86	1 2 5 3 6 7	ditgswap	$⊢ φ \to \int_{A}^{C} D d x = - \int_{C}^{A} D d x$
87	86	oveq2d	$⊢ φ \to \int_{C}^{A} D d x + \int_{A}^{C} D d x = \int_{C}^{A} D d x + (- \int_{C}^{A} D d x)$
88	54	negidd	$⊢ φ \to \int_{C}^{A} D d x + (- \int_{C}^{A} D d x) = 0$
89	87 88	eqtrd	$⊢ φ \to \int_{C}^{A} D d x + \int_{A}^{C} D d x = 0$
90	89	oveq2d	$⊢ φ \to \int_{B}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{C} D d x = \int_{B}^{C} D d x + 0$
91	32	addridd	$⊢ φ \to \int_{B}^{C} D d x + 0 = \int_{B}^{C} D d x$
92	85 90 91	3eqtrd	$⊢ φ \to \int_{B}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{C} D d x = \int_{B}^{C} D d x$
93	92	ad2antrr	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{B}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{C} D d x = \int_{B}^{C} D d x$
94	84 93	eqtr2d	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{B}^{C} D d x = \int_{B}^{A} D d x + \int_{A}^{C} D d x$
95	94	oveq2d	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{A}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x$
96	77	ad2antrr	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{A}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{C} D d x = \int_{A}^{C} D d x$
97	95 96	eqtr2d	$⊢ ((φ \land C \leq A) \land B \leq C) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
98	97	adantllr	$⊢ (((φ \land B \leq A) \land C \leq A) \land B \leq C) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
99		ancom	$⊢ (B \leq A \land C \leq B) \leftrightarrow (C \leq B \land B \leq A)$
100	1 2 5 4 3 6 7 99	ditgsplitlem	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{C}^{A} D d x = \int_{C}^{B} D d x + \int_{B}^{A} D d x$
101	100	oveq1d	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{C}^{A} D d x + \int_{A}^{B} D d x = \int_{C}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{B} D d x$
102	31 74 55	addassd	$⊢ φ \to \int_{C}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{B} D d x = \int_{C}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{B} D d x$
103	1 2 4 3 6 7	ditgswap	$⊢ φ \to \int_{A}^{B} D d x = - \int_{B}^{A} D d x$
104	103	oveq2d	$⊢ φ \to \int_{B}^{A} D d x + \int_{A}^{B} D d x = \int_{B}^{A} D d x + (- \int_{B}^{A} D d x)$
105	74	negidd	$⊢ φ \to \int_{B}^{A} D d x + (- \int_{B}^{A} D d x) = 0$
106	104 105	eqtrd	$⊢ φ \to \int_{B}^{A} D d x + \int_{A}^{B} D d x = 0$
107	106	oveq2d	$⊢ φ \to \int_{C}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{B} D d x = \int_{C}^{B} D d x + 0$
108	31	addridd	$⊢ φ \to \int_{C}^{B} D d x + 0 = \int_{C}^{B} D d x$
109	102 107 108	3eqtrd	$⊢ φ \to \int_{C}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{B} D d x = \int_{C}^{B} D d x$
110	109	ad2antrr	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{C}^{B} D d x + \int_{B}^{A} D d x + \int_{A}^{B} D d x = \int_{C}^{B} D d x$
111	101 110	eqtr2d	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{C}^{B} D d x = \int_{C}^{A} D d x + \int_{A}^{B} D d x$
112	111	oveq2d	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x = \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x$
113	58	ad2antrr	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{A}^{C} D d x + \int_{C}^{A} D d x + \int_{A}^{B} D d x = \int_{A}^{B} D d x$
114	112 113	eqtr2d	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{A}^{B} D d x = \int_{A}^{C} D d x + \int_{C}^{B} D d x$
115	114	oveq1d	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{A}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x$
116	40	ad2antrr	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{A}^{C} D d x + \int_{C}^{B} D d x + \int_{B}^{C} D d x = \int_{A}^{C} D d x$
117	115 116	eqtr2d	$⊢ ((φ \land B \leq A) \land C \leq B) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
118	117	adantlr	$⊢ (((φ \land B \leq A) \land C \leq A) \land C \leq B) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
119	80 81 98 118	lecasei	$⊢ ((φ \land B \leq A) \land C \leq A) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
120	64 65 79 119	lecasei	$⊢ (φ \land B \leq A) \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$
121	11 15 63 120	lecasei	$⊢ φ \to \int_{A}^{C} D d x = \int_{A}^{B} D d x + \int_{B}^{C} D d x$

Metamath Proof Explorer

Theorem ditgsplit

Proof