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