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 𝑦