Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶 ) ) |
2 |
|
oveq1 |
⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) ) |
3 |
|
itgeq1 |
⊢ ( ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) |
4 |
2 3
|
syl |
⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) |
5 |
|
oveq2 |
⊢ ( 𝐴 = 𝐵 → ( 𝐶 (,) 𝐴 ) = ( 𝐶 (,) 𝐵 ) ) |
6 |
|
itgeq1 |
⊢ ( ( 𝐶 (,) 𝐴 ) = ( 𝐶 (,) 𝐵 ) → ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 ) |
7 |
5 6
|
syl |
⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 ) |
8 |
7
|
negeqd |
⊢ ( 𝐴 = 𝐵 → - ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 = - ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 ) |
9 |
1 4 8
|
ifbieq12d |
⊢ ( 𝐴 = 𝐵 → if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 ) = if ( 𝐵 ≤ 𝐶 , ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 ) ) |
10 |
|
df-ditg |
⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = if ( 𝐴 ≤ 𝐶 , ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐴 ) 𝐷 d 𝑥 ) |
11 |
|
df-ditg |
⊢ ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 = if ( 𝐵 ≤ 𝐶 , ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 , - ∫ ( 𝐶 (,) 𝐵 ) 𝐷 d 𝑥 ) |
12 |
9 10 11
|
3eqtr4g |
⊢ ( 𝐴 = 𝐵 → ⨜ [ 𝐴 → 𝐶 ] 𝐷 d 𝑥 = ⨜ [ 𝐵 → 𝐶 ] 𝐷 d 𝑥 ) |