Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
ditgsplit.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
ditgsplit.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 [,] 𝑌 ) )
ditgsplit.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑋 [,] 𝑌 ) )
ditgsplit.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 [,] 𝑌 ) )
ditgsplit.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐷 ∈ 𝑉 )
ditgsplit.i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ 𝐿1 )
Assertion ditgsplit ( 𝜑 → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ( ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥 + ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) )

Proof

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