Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
|- ( A = B -> ( A <_ C <-> B <_ C ) ) |
2 |
|
oveq1 |
|- ( A = B -> ( A (,) C ) = ( B (,) C ) ) |
3 |
|
itgeq1 |
|- ( ( A (,) C ) = ( B (,) C ) -> S. ( A (,) C ) D _d x = S. ( B (,) C ) D _d x ) |
4 |
2 3
|
syl |
|- ( A = B -> S. ( A (,) C ) D _d x = S. ( B (,) C ) D _d x ) |
5 |
|
oveq2 |
|- ( A = B -> ( C (,) A ) = ( C (,) B ) ) |
6 |
|
itgeq1 |
|- ( ( C (,) A ) = ( C (,) B ) -> S. ( C (,) A ) D _d x = S. ( C (,) B ) D _d x ) |
7 |
5 6
|
syl |
|- ( A = B -> S. ( C (,) A ) D _d x = S. ( C (,) B ) D _d x ) |
8 |
7
|
negeqd |
|- ( A = B -> -u S. ( C (,) A ) D _d x = -u S. ( C (,) B ) D _d x ) |
9 |
1 4 8
|
ifbieq12d |
|- ( A = B -> if ( A <_ C , S. ( A (,) C ) D _d x , -u S. ( C (,) A ) D _d x ) = if ( B <_ C , S. ( B (,) C ) D _d x , -u S. ( C (,) B ) D _d x ) ) |
10 |
|
df-ditg |
|- S_ [ A -> C ] D _d x = if ( A <_ C , S. ( A (,) C ) D _d x , -u S. ( C (,) A ) D _d x ) |
11 |
|
df-ditg |
|- S_ [ B -> C ] D _d x = if ( B <_ C , S. ( B (,) C ) D _d x , -u S. ( C (,) B ) D _d x ) |
12 |
9 10 11
|
3eqtr4g |
|- ( A = B -> S_ [ A -> C ] D _d x = S_ [ B -> C ] D _d x ) |