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	|- F/_ y C
	cbvditg.3	|- F/_ x D
Assertion	cbvditg	|- S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y

Proof

Step	Hyp	Ref	Expression
1		cbvditg.1	|- ( x = y -> C = D )
2		cbvditg.2	|- F/_ y C
3		cbvditg.3	|- F/_ x D
4		biid	|- ( A <_ B <-> A <_ B )
5	1 2 3	cbvitg	|- S. ( A (,) B ) C _d x = S. ( A (,) B ) D _d y
6	1 2 3	cbvitg	|- S. ( B (,) A ) C _d x = S. ( B (,) A ) D _d y
7	6	negeqi	|- -u S. ( B (,) A ) C _d x = -u S. ( B (,) A ) D _d y
8	4 5 7	ifbieq12i	|- if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x ) = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y )
9		df-ditg	|- S_ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
10		df-ditg	|- S_ [ A -> B ] D _d y = if ( A <_ B , S. ( A (,) B ) D _d y , -u S. ( B (,) A ) D _d y )
11	8 9 10	3eqtr4i	|- S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d y