Metamath Proof Explorer


Theorem fsumf1o

Description: Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses fsumf1o.1 ( 𝑘 = 𝐺𝐵 = 𝐷 )
fsumf1o.2 ( 𝜑𝐶 ∈ Fin )
fsumf1o.3 ( 𝜑𝐹 : 𝐶1-1-onto𝐴 )
fsumf1o.4 ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
fsumf1o.5 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
Assertion fsumf1o ( 𝜑 → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 )

Proof

Step Hyp Ref Expression
1 fsumf1o.1 ( 𝑘 = 𝐺𝐵 = 𝐷 )
2 fsumf1o.2 ( 𝜑𝐶 ∈ Fin )
3 fsumf1o.3 ( 𝜑𝐹 : 𝐶1-1-onto𝐴 )
4 fsumf1o.4 ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
5 fsumf1o.5 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
6 sum0 Σ 𝑘 ∈ ∅ 𝐵 = 0
7 f1oeq2 ( 𝐶 = ∅ → ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : ∅ –1-1-onto𝐴 ) )
8 3 7 syl5ibcom ( 𝜑 → ( 𝐶 = ∅ → 𝐹 : ∅ –1-1-onto𝐴 ) )
9 8 imp ( ( 𝜑𝐶 = ∅ ) → 𝐹 : ∅ –1-1-onto𝐴 )
10 f1ofo ( 𝐹 : ∅ –1-1-onto𝐴𝐹 : ∅ –onto𝐴 )
11 fo00 ( 𝐹 : ∅ –onto𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
12 11 simprbi ( 𝐹 : ∅ –onto𝐴𝐴 = ∅ )
13 9 10 12 3syl ( ( 𝜑𝐶 = ∅ ) → 𝐴 = ∅ )
14 13 sumeq1d ( ( 𝜑𝐶 = ∅ ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
15 simpr ( ( 𝜑𝐶 = ∅ ) → 𝐶 = ∅ )
16 15 sumeq1d ( ( 𝜑𝐶 = ∅ ) → Σ 𝑛𝐶 𝐷 = Σ 𝑛 ∈ ∅ 𝐷 )
17 sum0 Σ 𝑛 ∈ ∅ 𝐷 = 0
18 16 17 eqtrdi ( ( 𝜑𝐶 = ∅ ) → Σ 𝑛𝐶 𝐷 = 0 )
19 6 14 18 3eqtr4a ( ( 𝜑𝐶 = ∅ ) → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 )
20 19 ex ( 𝜑 → ( 𝐶 = ∅ → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 ) )
21 2fveq3 ( 𝑚 = ( 𝑓𝑛 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓𝑛 ) ) ) )
22 simprl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℕ )
23 simprr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 )
24 f1of ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : 𝐶𝐴 )
25 3 24 syl ( 𝜑𝐹 : 𝐶𝐴 )
26 25 ffvelrnda ( ( 𝜑𝑚𝐶 ) → ( 𝐹𝑚 ) ∈ 𝐴 )
27 5 fmpttd ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ℂ )
28 27 ffvelrnda ( ( 𝜑 ∧ ( 𝐹𝑚 ) ∈ 𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
29 26 28 syldan ( ( 𝜑𝑚𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
30 29 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑚𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
31 f1oco ( ( 𝐹 : 𝐶1-1-onto𝐴𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐴 )
32 3 23 31 syl2an2r ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐴 )
33 f1of ( ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐴 → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
34 32 33 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
35 fvco3 ( ( ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) )
36 34 35 sylan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) )
37 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
38 37 ad2antll ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
39 fvco3 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓𝑛 ) ) )
40 38 39 sylan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓𝑛 ) ) )
41 40 fveq2d ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓𝑛 ) ) ) )
42 36 41 eqtrd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓𝑛 ) ) ) )
43 21 22 23 30 42 fsum ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → Σ 𝑚𝐶 ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) = ( seq 1 ( + , ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
44 25 ffvelrnda ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) ∈ 𝐴 )
45 4 44 eqeltrrd ( ( 𝜑𝑛𝐶 ) → 𝐺𝐴 )
46 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
47 1 46 fvmpti ( 𝐺𝐴 → ( ( 𝑘𝐴𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
48 45 47 syl ( ( 𝜑𝑛𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
49 4 fveq2d ( ( 𝜑𝑛𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ 𝐺 ) )
50 eqid ( 𝑛𝐶𝐷 ) = ( 𝑛𝐶𝐷 )
51 50 fvmpt2i ( 𝑛𝐶 → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
52 51 adantl ( ( 𝜑𝑛𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
53 48 49 52 3eqtr4rd ( ( 𝜑𝑛𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) )
54 53 ralrimiva ( 𝜑 → ∀ 𝑛𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) )
55 nffvmpt1 𝑛 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 )
56 55 nfeq1 𝑛 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) )
57 fveq2 ( 𝑛 = 𝑚 → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) )
58 2fveq3 ( 𝑛 = 𝑚 → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
59 57 58 eqeq12d ( 𝑛 = 𝑚 → ( ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) ↔ ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ) )
60 56 59 rspc ( 𝑚𝐶 → ( ∀ 𝑛𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ) )
61 54 60 mpan9 ( ( 𝜑𝑚𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
62 61 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑚𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
63 62 sumeq2dv ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → Σ 𝑚𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = Σ 𝑚𝐶 ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
64 fveq2 ( 𝑚 = ( ( 𝐹𝑓 ) ‘ 𝑛 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) )
65 27 adantr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ℂ )
66 65 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) ∈ ℂ )
67 64 22 32 66 36 fsum ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
68 43 63 67 3eqtr4rd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = Σ 𝑚𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) )
69 sumfc Σ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = Σ 𝑘𝐴 𝐵
70 sumfc Σ 𝑚𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = Σ 𝑛𝐶 𝐷
71 68 69 70 3eqtr3g ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 )
72 71 expr ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 ) )
73 72 exlimdv ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 ) )
74 73 expimpd ( 𝜑 → ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 ) )
75 fz1f1o ( 𝐶 ∈ Fin → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) )
76 2 75 syl ( 𝜑 → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) )
77 20 74 76 mpjaod ( 𝜑 → Σ 𝑘𝐴 𝐵 = Σ 𝑛𝐶 𝐷 )