Metamath Proof Explorer


Theorem cbvsumv

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Hypothesis cbvsum.1 j = k B = C
Assertion cbvsumv j A B = k A C

Proof

Step Hyp Ref Expression
1 cbvsum.1 j = k B = C
2 1 cbvcsbv n / j B = n / k C
3 2 a1i n / j B = n / k C
4 3 ifeq1d if n A n / j B 0 = if n A n / k C 0
5 4 mpteq2dv n if n A n / j B 0 = n if n A n / k C 0
6 5 seqeq3d seq m + n if n A n / j B 0 = seq m + n if n A n / k C 0
7 6 breq1d seq m + n if n A n / j B 0 x seq m + n if n A n / k C 0 x
8 7 mptru seq m + n if n A n / j B 0 x seq m + n if n A n / k C 0 x
9 8 anbi2i A m seq m + n if n A n / j B 0 x A m seq m + n if n A n / k C 0 x
10 9 rexbii m A m seq m + n if n A n / j B 0 x m A m seq m + n if n A n / k C 0 x
11 1 cbvcsbv f n / j B = f n / k C
12 11 mpteq2i n f n / j B = n f n / k C
13 12 a1i n f n / j B = n f n / k C
14 13 seqeq3d seq 1 + n f n / j B = seq 1 + n f n / k C
15 14 mptru seq 1 + n f n / j B = seq 1 + n f n / k C
16 15 fveq1i seq 1 + n f n / j B m = seq 1 + n f n / k C m
17 16 eqeq2i x = seq 1 + n f n / j B m x = seq 1 + n f n / k C m
18 17 anbi2i f : 1 m 1-1 onto A x = seq 1 + n f n / j B m f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
19 18 exbii f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
20 19 rexbii m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
21 10 20 orbi12i m A m seq m + n if n A n / j B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
22 21 iotabii ι x | m A m seq m + n if n A n / j B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m = ι x | m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
23 df-sum j A B = ι x | m A m seq m + n if n A n / j B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m
24 df-sum k A C = ι x | m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
25 22 23 24 3eqtr4i j A B = k A C