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 
|- ( ph -> X e. RR )
ditgsplit.y 
|- ( ph -> Y e. RR )
ditgsplit.a 
|- ( ph -> A e. ( X [,] Y ) )
ditgsplit.b 
|- ( ph -> B e. ( X [,] Y ) )
ditgsplit.c 
|- ( ph -> C e. ( X [,] Y ) )
ditgsplit.d 
|- ( ( ph /\ x e. ( X (,) Y ) ) -> D e. V )
ditgsplit.i 
|- ( ph -> ( x e. ( X (,) Y ) |-> D ) e. L^1 )
Assertion ditgsplit 
|- ( ph -> S_ [ A -> C ] D _d x = ( S_ [ A -> B ] D _d x + S_ [ B -> C ] D _d x ) )

Proof

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