ditgsplit - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ditgsplit		Structured version Visualization version GIF version

Theorem ditgsplit 23966

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

**Hypotheses**
Ref	Expression
ditgsplit.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
ditgsplit.y	⊢ (𝜑 → 𝑌 ∈ ℝ)
ditgsplit.a	⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))
ditgsplit.b	⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))
ditgsplit.c	⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌))
ditgsplit.d	⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉)
ditgsplit.i	⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿¹)

**Assertion**
Ref	Expression
ditgsplit	⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐶 𝜑,𝑥 𝑥,𝑉 𝑥,𝑋 𝑥,𝑌 Allowed substitution hint: 𝐷(𝑥)

**Proof of Theorem ditgsplit**
Step	Hyp	Ref	Expression
1		ditgsplit.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))
2		ditgsplit.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℝ)
3		ditgsplit.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ℝ)
4		elicc2 12487	. . . . 5 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌)))
5	2, 3, 4	syl2anc 580	. . . 4 ⊢ (𝜑 → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌)))
6	1, 5	mpbid 224	. . 3 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))
7	6	simp1d 1173	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
8		ditgsplit.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))
9		elicc2 12487	. . . . 5 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌)))
10	2, 3, 9	syl2anc 580	. . . 4 ⊢ (𝜑 → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌)))
11	8, 10	mpbid 224	. . 3 ⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))
12	11	simp1d 1173	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
13	7	adantr 473	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ)
14		ditgsplit.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌))
15		elicc2 12487	. . . . . . 7 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐶 ∈ (𝑋[,]𝑌) ↔ (𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌)))
16	2, 3, 15	syl2anc 580	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ (𝑋[,]𝑌) ↔ (𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌)))
17	14, 16	mpbid 224	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 𝑋 ≤ 𝐶 ∧ 𝐶 ≤ 𝑌))
18	17	simp1d 1173	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
19	18	adantr 473	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐶 ∈ ℝ)
20	12	ad2antrr 718	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 ≤ 𝐶) → 𝐵 ∈ ℝ)
21	18	ad2antrr 718	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 ≤ 𝐶) → 𝐶 ∈ ℝ)
22		ditgsplit.d	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉)
23		ditgsplit.i	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿¹)
24		biid 253	. . . . . 6 ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))
25	2, 3, 1, 8, 14, 22, 23, 24	ditgsplitlem 23965	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐵 ≤ 𝐶) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
26	25	adantlr 707	. . . 4 ⊢ ((((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 ≤ 𝐶) ∧ 𝐵 ≤ 𝐶) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
27		biid 253	. . . . . . . 8 ⊢ ((𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))
28	2, 3, 1, 14, 8, 22, 23, 27	ditgsplitlem 23965	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥))
29	28	oveq1d 6893	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 ≤ 𝐵) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
30	2, 3, 1, 14, 22, 23	ditgcl 23963	. . . . . . . . 9 ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 ∈ ℂ)
31	2, 3, 14, 8, 22, 23	ditgcl 23963	. . . . . . . . 9 ⊢ (𝜑 → ⨜[𝐶 → 𝐵]𝐷 d𝑥 ∈ ℂ)
32	2, 3, 8, 14, 22, 23	ditgcl 23963	. . . . . . . . 9 ⊢ (𝜑 → ⨜[𝐵 → 𝐶]𝐷 d𝑥 ∈ ℂ)
33	30, 31, 32	addassd 10351	. . . . . . . 8 ⊢ (𝜑 → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)))
34	2, 3, 14, 8, 22, 23	ditgswap 23964	. . . . . . . . . . 11 ⊢ (𝜑 → ⨜[𝐵 → 𝐶]𝐷 d𝑥 = -⨜[𝐶 → 𝐵]𝐷 d𝑥)
35	34	oveq2d 6894	. . . . . . . . . 10 ⊢ (𝜑 → (⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = (⨜[𝐶 → 𝐵]𝐷 d𝑥 + -⨜[𝐶 → 𝐵]𝐷 d𝑥))
36	31	negidd 10674	. . . . . . . . . 10 ⊢ (𝜑 → (⨜[𝐶 → 𝐵]𝐷 d𝑥 + -⨜[𝐶 → 𝐵]𝐷 d𝑥) = 0)
37	35, 36	eqtrd 2833	. . . . . . . . 9 ⊢ (𝜑 → (⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = 0)
38	37	oveq2d 6894	. . . . . . . 8 ⊢ (𝜑 → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥)) = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + 0))
39	30	addid1d 10526	. . . . . . . 8 ⊢ (𝜑 → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + 0) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
40	33, 38, 39	3eqtrd 2837	. . . . . . 7 ⊢ (𝜑 → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
41	40	ad2antrr 718	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 ≤ 𝐵) → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
42	29, 41	eqtr2d 2834	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
43	42	adantllr 711	. . . 4 ⊢ ((((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 ≤ 𝐶) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
44	20, 21, 26, 43	lecasei 10433	. . 3 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐴 ≤ 𝐶) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
45	40	ad2antrr 718	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
46		ancom 453	. . . . . . . 8 ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐴) ↔ (𝐶 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))
47	2, 3, 14, 1, 8, 22, 23, 46	ditgsplitlem 23965	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → ⨜[𝐶 → 𝐵]𝐷 d𝑥 = (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥))
48	47	oveq2d 6894	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)))
49	2, 3, 1, 14, 22, 23	ditgswap 23964	. . . . . . . . . . 11 ⊢ (𝜑 → ⨜[𝐶 → 𝐴]𝐷 d𝑥 = -⨜[𝐴 → 𝐶]𝐷 d𝑥)
50	49	oveq2d 6894	. . . . . . . . . 10 ⊢ (𝜑 → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + -⨜[𝐴 → 𝐶]𝐷 d𝑥))
51	30	negidd 10674	. . . . . . . . . 10 ⊢ (𝜑 → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + -⨜[𝐴 → 𝐶]𝐷 d𝑥) = 0)
52	50, 51	eqtrd 2833	. . . . . . . . 9 ⊢ (𝜑 → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) = 0)
53	52	oveq1d 6893	. . . . . . . 8 ⊢ (𝜑 → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = (0 + ⨜[𝐴 → 𝐵]𝐷 d𝑥))
54	2, 3, 14, 1, 22, 23	ditgcl 23963	. . . . . . . . 9 ⊢ (𝜑 → ⨜[𝐶 → 𝐴]𝐷 d𝑥 ∈ ℂ)
55	2, 3, 1, 8, 22, 23	ditgcl 23963	. . . . . . . . 9 ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 ∈ ℂ)
56	30, 54, 55	addassd 10351	. . . . . . . 8 ⊢ (𝜑 → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)))
57	55	addid2d 10527	. . . . . . . 8 ⊢ (𝜑 → (0 + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
58	53, 56, 57	3eqtr3d 2841	. . . . . . 7 ⊢ (𝜑 → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)) = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
59	58	ad2antrr 718	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)) = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
60	48, 59	eqtrd 2833	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
61	60	oveq1d 6893	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
62	45, 61	eqtr3d 2835	. . 3 ⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝐶 ≤ 𝐴) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
63	13, 19, 44, 62	lecasei 10433	. 2 ⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
64	7	adantr 473	. . 3 ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝐴 ∈ ℝ)
65	18	adantr 473	. . 3 ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝐶 ∈ ℝ)
66		biid 253	. . . . . 6 ⊢ ((𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶) ↔ (𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶))
67	2, 3, 8, 1, 14, 22, 23, 66	ditgsplitlem 23965	. . . . 5 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐴 ≤ 𝐶) → ⨜[𝐵 → 𝐶]𝐷 d𝑥 = (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥))
68	67	oveq2d 6894	. . . 4 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐴 ≤ 𝐶) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)))
69	2, 3, 1, 8, 22, 23	ditgswap 23964	. . . . . . . . 9 ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐷 d𝑥 = -⨜[𝐴 → 𝐵]𝐷 d𝑥)
70	69	oveq2d 6894	. . . . . . . 8 ⊢ (𝜑 → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + -⨜[𝐴 → 𝐵]𝐷 d𝑥))
71	55	negidd 10674	. . . . . . . 8 ⊢ (𝜑 → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + -⨜[𝐴 → 𝐵]𝐷 d𝑥) = 0)
72	70, 71	eqtrd 2833	. . . . . . 7 ⊢ (𝜑 → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) = 0)
73	72	oveq1d 6893	. . . . . 6 ⊢ (𝜑 → ((⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = (0 + ⨜[𝐴 → 𝐶]𝐷 d𝑥))
74	2, 3, 8, 1, 22, 23	ditgcl 23963	. . . . . . 7 ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐷 d𝑥 ∈ ℂ)
75	55, 74, 30	addassd 10351	. . . . . 6 ⊢ (𝜑 → ((⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)))
76	30	addid2d 10527	. . . . . 6 ⊢ (𝜑 → (0 + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
77	73, 75, 76	3eqtr3d 2841	. . . . 5 ⊢ (𝜑 → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
78	77	ad2antrr 718	. . . 4 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐴 ≤ 𝐶) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
79	68, 78	eqtr2d 2834	. . 3 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐴 ≤ 𝐶) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
80	12	ad2antrr 718	. . . 4 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐴) → 𝐵 ∈ ℝ)
81	18	ad2antrr 718	. . . 4 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐴) → 𝐶 ∈ ℝ)
82		ancom 453	. . . . . . . . . 10 ⊢ ((𝐶 ≤ 𝐴 ∧ 𝐵 ≤ 𝐶) ↔ (𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴))
83	2, 3, 8, 14, 1, 22, 23, 82	ditgsplitlem 23965	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → ⨜[𝐵 → 𝐴]𝐷 d𝑥 = (⨜[𝐵 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥))
84	83	oveq1d 6893	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = ((⨜[𝐵 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐶]𝐷 d𝑥))
85	32, 54, 30	addassd 10351	. . . . . . . . . 10 ⊢ (𝜑 → ((⨜[𝐵 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = (⨜[𝐵 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)))
86	2, 3, 14, 1, 22, 23	ditgswap 23964	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = -⨜[𝐶 → 𝐴]𝐷 d𝑥)
87	86	oveq2d 6894	. . . . . . . . . . . 12 ⊢ (𝜑 → (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = (⨜[𝐶 → 𝐴]𝐷 d𝑥 + -⨜[𝐶 → 𝐴]𝐷 d𝑥))
88	54	negidd 10674	. . . . . . . . . . . 12 ⊢ (𝜑 → (⨜[𝐶 → 𝐴]𝐷 d𝑥 + -⨜[𝐶 → 𝐴]𝐷 d𝑥) = 0)
89	87, 88	eqtrd 2833	. . . . . . . . . . 11 ⊢ (𝜑 → (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = 0)
90	89	oveq2d 6894	. . . . . . . . . 10 ⊢ (𝜑 → (⨜[𝐵 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)) = (⨜[𝐵 → 𝐶]𝐷 d𝑥 + 0))
91	32	addid1d 10526	. . . . . . . . . 10 ⊢ (𝜑 → (⨜[𝐵 → 𝐶]𝐷 d𝑥 + 0) = ⨜[𝐵 → 𝐶]𝐷 d𝑥)
92	85, 90, 91	3eqtrd 2837	. . . . . . . . 9 ⊢ (𝜑 → ((⨜[𝐵 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = ⨜[𝐵 → 𝐶]𝐷 d𝑥)
93	92	ad2antrr 718	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → ((⨜[𝐵 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐶]𝐷 d𝑥) = ⨜[𝐵 → 𝐶]𝐷 d𝑥)
94	84, 93	eqtr2d 2834	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → ⨜[𝐵 → 𝐶]𝐷 d𝑥 = (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥))
95	94	oveq2d 6894	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)))
96	77	ad2antrr 718	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐶]𝐷 d𝑥)) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
97	95, 96	eqtr2d 2834	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
98	97	adantllr 711	. . . 4 ⊢ ((((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐴) ∧ 𝐵 ≤ 𝐶) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
99		ancom 453	. . . . . . . . . . . 12 ⊢ ((𝐵 ≤ 𝐴 ∧ 𝐶 ≤ 𝐵) ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))
100	2, 3, 14, 8, 1, 22, 23, 99	ditgsplitlem 23965	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐶 → 𝐴]𝐷 d𝑥 = (⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥))
101	100	oveq1d 6893	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = ((⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐵]𝐷 d𝑥))
102	31, 74, 55	addassd 10351	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = (⨜[𝐶 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)))
103	2, 3, 8, 1, 22, 23	ditgswap 23964	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = -⨜[𝐵 → 𝐴]𝐷 d𝑥)
104	103	oveq2d 6894	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = (⨜[𝐵 → 𝐴]𝐷 d𝑥 + -⨜[𝐵 → 𝐴]𝐷 d𝑥))
105	74	negidd 10674	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⨜[𝐵 → 𝐴]𝐷 d𝑥 + -⨜[𝐵 → 𝐴]𝐷 d𝑥) = 0)
106	104, 105	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = 0)
107	106	oveq2d 6894	. . . . . . . . . . . 12 ⊢ (𝜑 → (⨜[𝐶 → 𝐵]𝐷 d𝑥 + (⨜[𝐵 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)) = (⨜[𝐶 → 𝐵]𝐷 d𝑥 + 0))
108	31	addid1d 10526	. . . . . . . . . . . 12 ⊢ (𝜑 → (⨜[𝐶 → 𝐵]𝐷 d𝑥 + 0) = ⨜[𝐶 → 𝐵]𝐷 d𝑥)
109	102, 107, 108	3eqtrd 2837	. . . . . . . . . . 11 ⊢ (𝜑 → ((⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = ⨜[𝐶 → 𝐵]𝐷 d𝑥)
110	109	ad2antrr 718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ((⨜[𝐶 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐴]𝐷 d𝑥) + ⨜[𝐴 → 𝐵]𝐷 d𝑥) = ⨜[𝐶 → 𝐵]𝐷 d𝑥)
111	101, 110	eqtr2d 2834	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐶 → 𝐵]𝐷 d𝑥 = (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥))
112	111	oveq2d 6894	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)))
113	58	ad2antrr 718	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → (⨜[𝐴 → 𝐶]𝐷 d𝑥 + (⨜[𝐶 → 𝐴]𝐷 d𝑥 + ⨜[𝐴 → 𝐵]𝐷 d𝑥)) = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
114	112, 113	eqtr2d 2834	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = (⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥))
115	114	oveq1d 6893	. . . . . 6 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
116	40	ad2antrr 718	. . . . . 6 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ((⨜[𝐴 → 𝐶]𝐷 d𝑥 + ⨜[𝐶 → 𝐵]𝐷 d𝑥) + ⨜[𝐵 → 𝐶]𝐷 d𝑥) = ⨜[𝐴 → 𝐶]𝐷 d𝑥)
117	115, 116	eqtr2d 2834	. . . . 5 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
118	117	adantlr 707	. . . 4 ⊢ ((((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐴) ∧ 𝐶 ≤ 𝐵) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
119	80, 81, 98, 118	lecasei 10433	. . 3 ⊢ (((𝜑 ∧ 𝐵 ≤ 𝐴) ∧ 𝐶 ≤ 𝐴) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
120	64, 65, 79, 119	lecasei 10433	. 2 ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
121	7, 12, 63, 120	lecasei 10433	1 ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 class class class wbr 4843 ↦ cmpt 4922 (class class class)co 6878 ℝcr 10223 0cc0 10224 + caddc 10227 ≤ cle 10364 -cneg 10557 (,)cioo 12424 [,]cicc 12427 𝐿¹cibl 23725 ⨜cdit 23951

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-inf2 8788 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301 ax-pre-sup 10302 ax-addf 10303

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-fal 1667 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-symdif 4041 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-int 4668 df-iun 4712 df-disj 4812 df-br 4844 df-opab 4906 df-mpt 4923 df-tr 4946 df-id 5220 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-se 5272 df-we 5273 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-pred 5898 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-isom 6110 df-riota 6839 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-of 7131 df-ofr 7132 df-om 7300 df-1st 7401 df-2nd 7402 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-1o 7799 df-2o 7800 df-oadd 7803 df-er 7982 df-map 8097 df-pm 8098 df-en 8196 df-dom 8197 df-sdom 8198 df-fin 8199 df-fi 8559 df-sup 8590 df-inf 8591 df-oi 8657 df-card 9051 df-cda 9278 df-pnf 10365 df-mnf 10366 df-xr 10367 df-ltxr 10368 df-le 10369 df-sub 10558 df-neg 10559 df-div 10977 df-nn 11313 df-2 11376 df-3 11377 df-4 11378 df-n0 11581 df-z 11667 df-uz 11931 df-q 12034 df-rp 12075 df-xneg 12193 df-xadd 12194 df-xmul 12195 df-ioo 12428 df-ico 12430 df-icc 12431 df-fz 12581 df-fzo 12721 df-fl 12848 df-mod 12924 df-seq 13056 df-exp 13115 df-hash 13371 df-cj 14180 df-re 14181 df-im 14182 df-sqrt 14316 df-abs 14317 df-clim 14560 df-rlim 14561 df-sum 14758 df-rest 16398 df-topgen 16419 df-psmet 20060 df-xmet 20061 df-met 20062 df-bl 20063 df-mopn 20064 df-top 21027 df-topon 21044 df-bases 21079 df-cmp 21519 df-ovol 23572 df-vol 23573 df-mbf 23727 df-itg1 23728 df-itg2 23729 df-ibl 23730 df-itg 23731 df-0p 23778 df-ditg 23952

This theorem is referenced by: itgsubstlem 24152

W3C validator