Metamath Proof Explorer

Theorem fsumf1of

Description: Re-index a finite sum using a bijection. Same as fsumf1o , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fsumf1of.1 
|- F/ k ph
fsumf1of.2 
|- F/ n ph
fsumf1of.3 
|- ( k = G -> B = D )
fsumf1of.4 
|- ( ph -> C e. Fin )
fsumf1of.5 
|- ( ph -> F : C -1-1-onto-> A )
fsumf1of.6 
|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
fsumf1of.7 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumf1of 
|- ( ph -> sum_ k e. A B = sum_ n e. C D )

Proof

Step Hyp Ref Expression
1 fsumf1of.1 
 |-  F/ k ph
2 fsumf1of.2 
 |-  F/ n ph
3 fsumf1of.3 
 |-  ( k = G -> B = D )
4 fsumf1of.4 
 |-  ( ph -> C e. Fin )
5 fsumf1of.5 
 |-  ( ph -> F : C -1-1-onto-> A )
6 fsumf1of.6 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) = G )
7 fsumf1of.7 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
8 csbeq1a 
 |-  ( k = i -> B = [_ i / k ]_ B )
9 nfcv 
 |-  F/_ i B
10 nfcsb1v 
 |-  F/_ k [_ i / k ]_ B
11 8 9 10 cbvsum 
 |-  sum_ k e. A B = sum_ i e. A [_ i / k ]_ B
12 11 a1i 
 |-  ( ph -> sum_ k e. A B = sum_ i e. A [_ i / k ]_ B )
13 nfv 
 |-  F/ k i = [_ j / n ]_ G
14 nfcv 
 |-  F/_ k [_ j / n ]_ D
15 10 14 nfeq 
 |-  F/ k [_ i / k ]_ B = [_ j / n ]_ D
16 13 15 nfim 
 |-  F/ k ( i = [_ j / n ]_ G -> [_ i / k ]_ B = [_ j / n ]_ D )
17 eqeq1 
 |-  ( k = i -> ( k = [_ j / n ]_ G <-> i = [_ j / n ]_ G ) )
18 8 eqeq1d 
 |-  ( k = i -> ( B = [_ j / n ]_ D <-> [_ i / k ]_ B = [_ j / n ]_ D ) )
19 17 18 imbi12d 
 |-  ( k = i -> ( ( k = [_ j / n ]_ G -> B = [_ j / n ]_ D ) <-> ( i = [_ j / n ]_ G -> [_ i / k ]_ B = [_ j / n ]_ D ) ) )
20 nfcv 
 |-  F/_ n k
21 nfcsb1v 
 |-  F/_ n [_ j / n ]_ G
22 20 21 nfeq 
 |-  F/ n k = [_ j / n ]_ G
23 nfcv 
 |-  F/_ n B
24 nfcsb1v 
 |-  F/_ n [_ j / n ]_ D
25 23 24 nfeq 
 |-  F/ n B = [_ j / n ]_ D
26 22 25 nfim 
 |-  F/ n ( k = [_ j / n ]_ G -> B = [_ j / n ]_ D )
27 csbeq1a 
 |-  ( n = j -> G = [_ j / n ]_ G )
28 27 eqeq2d 
 |-  ( n = j -> ( k = G <-> k = [_ j / n ]_ G ) )
29 csbeq1a 
 |-  ( n = j -> D = [_ j / n ]_ D )
30 29 eqeq2d 
 |-  ( n = j -> ( B = D <-> B = [_ j / n ]_ D ) )
31 28 30 imbi12d 
 |-  ( n = j -> ( ( k = G -> B = D ) <-> ( k = [_ j / n ]_ G -> B = [_ j / n ]_ D ) ) )
32 26 31 3 chvarfv 
 |-  ( k = [_ j / n ]_ G -> B = [_ j / n ]_ D )
33 16 19 32 chvarfv 
 |-  ( i = [_ j / n ]_ G -> [_ i / k ]_ B = [_ j / n ]_ D )
34 nfv 
 |-  F/ n j e. C
35 2 34 nfan 
 |-  F/ n ( ph /\ j e. C )
36 nfcv 
 |-  F/_ n ( F ` j )
37 36 21 nfeq 
 |-  F/ n ( F ` j ) = [_ j / n ]_ G
38 35 37 nfim 
 |-  F/ n ( ( ph /\ j e. C ) -> ( F ` j ) = [_ j / n ]_ G )
39 eleq1w 
 |-  ( n = j -> ( n e. C <-> j e. C ) )
40 39 anbi2d 
 |-  ( n = j -> ( ( ph /\ n e. C ) <-> ( ph /\ j e. C ) ) )
41 fveq2 
 |-  ( n = j -> ( F ` n ) = ( F ` j ) )
42 41 27 eqeq12d 
 |-  ( n = j -> ( ( F ` n ) = G <-> ( F ` j ) = [_ j / n ]_ G ) )
43 40 42 imbi12d 
 |-  ( n = j -> ( ( ( ph /\ n e. C ) -> ( F ` n ) = G ) <-> ( ( ph /\ j e. C ) -> ( F ` j ) = [_ j / n ]_ G ) ) )
44 38 43 6 chvarfv 
 |-  ( ( ph /\ j e. C ) -> ( F ` j ) = [_ j / n ]_ G )
45 nfv 
 |-  F/ k i e. A
46 1 45 nfan 
 |-  F/ k ( ph /\ i e. A )
47 10 nfel1 
 |-  F/ k [_ i / k ]_ B e. CC
48 46 47 nfim 
 |-  F/ k ( ( ph /\ i e. A ) -> [_ i / k ]_ B e. CC )
49 eleq1w 
 |-  ( k = i -> ( k e. A <-> i e. A ) )
50 49 anbi2d 
 |-  ( k = i -> ( ( ph /\ k e. A ) <-> ( ph /\ i e. A ) ) )
51 8 eleq1d 
 |-  ( k = i -> ( B e. CC <-> [_ i / k ]_ B e. CC ) )
52 50 51 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. A ) -> B e. CC ) <-> ( ( ph /\ i e. A ) -> [_ i / k ]_ B e. CC ) ) )
53 48 52 7 chvarfv 
 |-  ( ( ph /\ i e. A ) -> [_ i / k ]_ B e. CC )
54 33 4 5 44 53 fsumf1o 
 |-  ( ph -> sum_ i e. A [_ i / k ]_ B = sum_ j e. C [_ j / n ]_ D )
55 nfcv 
 |-  F/_ j D
56 29 55 24 cbvsum 
 |-  sum_ n e. C D = sum_ j e. C [_ j / n ]_ D
57 56 eqcomi 
 |-  sum_ j e. C [_ j / n ]_ D = sum_ n e. C D
58 57 a1i 
 |-  ( ph -> sum_ j e. C [_ j / n ]_ D = sum_ n e. C D )
59 12 54 58 3eqtrd 
 |-  ( ph -> sum_ k e. A B = sum_ n e. C D )