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 ⊢ x = y → C = D
cbvditg.2 ⊢ Ⅎ _ y C
cbvditg.3 ⊢ Ⅎ _ x D
Assertion cbvditg ⊢ ∫ A B C dx = ∫ A B D dy

Proof

Step Hyp Ref Expression
1 cbvditg.1 ⊢ x = y → C = D
2 cbvditg.2 ⊢ Ⅎ _ y C
3 cbvditg.3 ⊢ Ⅎ _ x D
4 biid ⊢ A ≤ B ↔ A ≤ B
5 1 2 3 cbvitg ⊢ ∫ A B C dx = ∫ A B D dy
6 1 2 3 cbvitg ⊢ ∫ B A C dx = ∫ B A D dy
7 6 negeqi ⊢ − ∫ B A C dx = − ∫ B A D dy
8 4 5 7 ifbieq12i ⊢ if A ≤ B ∫ A B C dx − ∫ B A C dx = if A ≤ B ∫ A B D dy − ∫ B A D dy
9 df-ditg ⊢ ∫ A B C dx = if A ≤ B ∫ A B C dx − ∫ B A C dx
10 df-ditg ⊢ ∫ A B D dy = if A ≤ B ∫ A B D dy − ∫ B A D dy
11 8 9 10 3eqtr4i ⊢ ∫ A B C dx = ∫ A B D dy