Metamath Proof Explorer

Theorem etransclem5

Description: A change of bound variable, often used in proofs for etransc . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion etransclem5 
|- ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( k e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = y -> ( x - j ) = ( y - j ) )
2 1 oveq1d 
 |-  ( x = y -> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( y - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) )
3 2 cbvmptv 
 |-  ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( y e. X |-> ( ( y - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) )
4 oveq2 
 |-  ( j = k -> ( y - j ) = ( y - k ) )
5 eqeq1 
 |-  ( j = k -> ( j = 0 <-> k = 0 ) )
6 5 ifbid 
 |-  ( j = k -> if ( j = 0 , ( P - 1 ) , P ) = if ( k = 0 , ( P - 1 ) , P ) )
7 4 6 oveq12d 
 |-  ( j = k -> ( ( y - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) = ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) )
8 7 mpteq2dv 
 |-  ( j = k -> ( y e. X |-> ( ( y - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( y e. X |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )
9 3 8 syl5eq 
 |-  ( j = k -> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) = ( y e. X |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )
10 9 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( k e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )