Theorem cbvditgdavw2

Description: Change bound variable and limits in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvditgdavw2.1	|- ( ph -> A = B )
	cbvditgdavw2.2	|- ( ph -> C = D )
	cbvditgdavw2.3	|- ( ( ph /\ x = y ) -> E = F )
Assertion	cbvditgdavw2	|- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d y )

Proof

Step	Hyp	Ref	Expression
1		cbvditgdavw2.1	|- ( ph -> A = B )
2		cbvditgdavw2.2	|- ( ph -> C = D )
3		cbvditgdavw2.3	|- ( ( ph /\ x = y ) -> E = F )
4	1 2	breq12d	|- ( ph -> ( A <_ C <-> B <_ D ) )
5	1	adantr	|- ( ( ph /\ x = y ) -> A = B )
6	2	adantr	|- ( ( ph /\ x = y ) -> C = D )
7	5 6	oveq12d	|- ( ( ph /\ x = y ) -> ( A (,) C ) = ( B (,) D ) )
8	3 7	cbvitgdavw2	|- ( ph -> S. ( A (,) C ) E _d x = S. ( B (,) D ) F _d y )
9	6 5	oveq12d	|- ( ( ph /\ x = y ) -> ( C (,) A ) = ( D (,) B ) )
10	3 9	cbvitgdavw2	|- ( ph -> S. ( C (,) A ) E _d x = S. ( D (,) B ) F _d y )
11	10	negeqd	|- ( ph -> -u S. ( C (,) A ) E _d x = -u S. ( D (,) B ) F _d y )
12	4 8 11	ifbieq12d	|- ( ph -> if ( A <_ C , S. ( A (,) C ) E _d x , -u S. ( C (,) A ) E _d x ) = if ( B <_ D , S. ( B (,) D ) F _d y , -u S. ( D (,) B ) F _d y ) )
13		df-ditg	|- S_ [ A -> C ] E _d x = if ( A <_ C , S. ( A (,) C ) E _d x , -u S. ( C (,) A ) E _d x )
14		df-ditg	|- S_ [ B -> D ] F _d y = if ( B <_ D , S. ( B (,) D ) F _d y , -u S. ( D (,) B ) F _d y )
15	12 13 14	3eqtr4g	|- ( ph -> S_ [ A -> C ] E _d x = S_ [ B -> D ] F _d y )