Step |
Hyp |
Ref |
Expression |
1 |
|
cbvditg.1 |
⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 ) |
2 |
|
cbvditg.2 |
⊢ Ⅎ 𝑦 𝐶 |
3 |
|
cbvditg.3 |
⊢ Ⅎ 𝑥 𝐷 |
4 |
|
biid |
⊢ ( 𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐵 ) |
5 |
1 2 3
|
cbvitg |
⊢ ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑦 |
6 |
1 2 3
|
cbvitg |
⊢ ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 = ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 |
7 |
6
|
negeqi |
⊢ - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 = - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 |
8 |
4 5 7
|
ifbieq12i |
⊢ if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ) = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑦 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 ) |
9 |
|
df-ditg |
⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐶 d 𝑥 ) |
10 |
|
df-ditg |
⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦 = if ( 𝐴 ≤ 𝐵 , ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑦 , - ∫ ( 𝐵 (,) 𝐴 ) 𝐷 d 𝑦 ) |
11 |
8 9 10
|
3eqtr4i |
⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑦 |