# 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 ) ) ) )`