Metamath Proof Explorer

Theorem etransclem11

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

Ref Expression
Assertion etransclem11 
|- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = m -> ( 0 ... n ) = ( 0 ... m ) )
2 1 oveq1d 
 |-  ( n = m -> ( ( 0 ... n ) ^m ( 0 ... M ) ) = ( ( 0 ... m ) ^m ( 0 ... M ) ) )
3 2 rabeqdv 
 |-  ( n = m -> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { c e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
4 fveq2 
 |-  ( j = k -> ( c ` j ) = ( c ` k ) )
5 4 cbvsumv 
 |-  sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( c ` k )
6 fveq1 
 |-  ( c = d -> ( c ` k ) = ( d ` k ) )
7 6 sumeq2sdv 
 |-  ( c = d -> sum_ k e. ( 0 ... M ) ( c ` k ) = sum_ k e. ( 0 ... M ) ( d ` k ) )
8 5 7 eqtrid 
 |-  ( c = d -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( d ` k ) )
9 8 eqeq1d 
 |-  ( c = d -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = n <-> sum_ k e. ( 0 ... M ) ( d ` k ) = n ) )
10 9 cbvrabv 
 |-  { c e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = n }
11 eqeq2 
 |-  ( n = m -> ( sum_ k e. ( 0 ... M ) ( d ` k ) = n <-> sum_ k e. ( 0 ... M ) ( d ` k ) = m ) )
12 11 rabbidv 
 |-  ( n = m -> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )
13 10 12 eqtrid 
 |-  ( n = m -> { c e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )
14 3 13 eqtrd 
 |-  ( n = m -> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } = { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )
15 14 cbvmptv 
 |-  ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )