Metamath Proof Explorer


Theorem cbvditg

Description: Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses cbvditg.1 ( 𝑥 = 𝑦𝐶 = 𝐷 )
cbvditg.2 𝑦 𝐶
cbvditg.3 𝑥 𝐷
Assertion cbvditg ⨜ [ 𝐴𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴𝐵 ] 𝐷 d 𝑦

Proof

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 𝑦