This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑦