# Metamath Proof Explorer

## Theorem summolem3

Description: Lemma for summo . (Contributed by Mario Carneiro, 29-Mar-2014)

Ref Expression
Hypotheses summo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)$
summo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
summo.3
summolem3.4
summolem3.5 ${⊢}{\phi }\to \left({M}\in ℕ\wedge {N}\in ℕ\right)$
summolem3.6 ${⊢}{\phi }\to {f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}$
summolem3.7 ${⊢}{\phi }\to {K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
Assertion summolem3 ${⊢}{\phi }\to seq1\left(+,{G}\right)\left({M}\right)=seq1\left(+,{H}\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 summo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)$
2 summo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 summo.3
4 summolem3.4
5 summolem3.5 ${⊢}{\phi }\to \left({M}\in ℕ\wedge {N}\in ℕ\right)$
6 summolem3.6 ${⊢}{\phi }\to {f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}$
7 summolem3.7 ${⊢}{\phi }\to {K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
8 addcl ${⊢}\left({m}\in ℂ\wedge {j}\in ℂ\right)\to {m}+{j}\in ℂ$
9 8 adantl ${⊢}\left({\phi }\wedge \left({m}\in ℂ\wedge {j}\in ℂ\right)\right)\to {m}+{j}\in ℂ$
10 addcom ${⊢}\left({m}\in ℂ\wedge {j}\in ℂ\right)\to {m}+{j}={j}+{m}$
11 10 adantl ${⊢}\left({\phi }\wedge \left({m}\in ℂ\wedge {j}\in ℂ\right)\right)\to {m}+{j}={j}+{m}$
12 addass ${⊢}\left({m}\in ℂ\wedge {j}\in ℂ\wedge {y}\in ℂ\right)\to {m}+{j}+{y}={m}+{j}+{y}$
13 12 adantl ${⊢}\left({\phi }\wedge \left({m}\in ℂ\wedge {j}\in ℂ\wedge {y}\in ℂ\right)\right)\to {m}+{j}+{y}={m}+{j}+{y}$
14 5 simpld ${⊢}{\phi }\to {M}\in ℕ$
15 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
16 14 15 eleqtrdi ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 1}$
17 ssidd ${⊢}{\phi }\to ℂ\subseteq ℂ$
18 f1ocnv ${⊢}{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}\to {{f}}^{-1}:{A}\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
19 6 18 syl ${⊢}{\phi }\to {{f}}^{-1}:{A}\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
20 f1oco ${⊢}\left({{f}}^{-1}:{A}\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\wedge {K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}\right)\to \left({{f}}^{-1}\circ {K}\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
21 19 7 20 syl2anc ${⊢}{\phi }\to \left({{f}}^{-1}\circ {K}\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
22 ovex ${⊢}\left(1\dots {N}\right)\in \mathrm{V}$
23 22 f1oen ${⊢}\left({{f}}^{-1}\circ {K}\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\to \left(1\dots {N}\right)\approx \left(1\dots {M}\right)$
24 21 23 syl ${⊢}{\phi }\to \left(1\dots {N}\right)\approx \left(1\dots {M}\right)$
25 fzfi ${⊢}\left(1\dots {N}\right)\in \mathrm{Fin}$
26 fzfi ${⊢}\left(1\dots {M}\right)\in \mathrm{Fin}$
27 hashen ${⊢}\left(\left(1\dots {N}\right)\in \mathrm{Fin}\wedge \left(1\dots {M}\right)\in \mathrm{Fin}\right)\to \left(\left|\left(1\dots {N}\right)\right|=\left|\left(1\dots {M}\right)\right|↔\left(1\dots {N}\right)\approx \left(1\dots {M}\right)\right)$
28 25 26 27 mp2an ${⊢}\left|\left(1\dots {N}\right)\right|=\left|\left(1\dots {M}\right)\right|↔\left(1\dots {N}\right)\approx \left(1\dots {M}\right)$
29 24 28 sylibr ${⊢}{\phi }\to \left|\left(1\dots {N}\right)\right|=\left|\left(1\dots {M}\right)\right|$
30 5 simprd ${⊢}{\phi }\to {N}\in ℕ$
31 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
32 hashfz1 ${⊢}{N}\in {ℕ}_{0}\to \left|\left(1\dots {N}\right)\right|={N}$
33 30 31 32 3syl ${⊢}{\phi }\to \left|\left(1\dots {N}\right)\right|={N}$
34 nnnn0 ${⊢}{M}\in ℕ\to {M}\in {ℕ}_{0}$
35 hashfz1 ${⊢}{M}\in {ℕ}_{0}\to \left|\left(1\dots {M}\right)\right|={M}$
36 14 34 35 3syl ${⊢}{\phi }\to \left|\left(1\dots {M}\right)\right|={M}$
37 29 33 36 3eqtr3rd ${⊢}{\phi }\to {M}={N}$
38 37 oveq2d ${⊢}{\phi }\to \left(1\dots {M}\right)=\left(1\dots {N}\right)$
39 38 f1oeq2d ${⊢}{\phi }\to \left(\left({{f}}^{-1}\circ {K}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)↔\left({{f}}^{-1}\circ {K}\right):\left(1\dots {N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\right)$
40 21 39 mpbird ${⊢}{\phi }\to \left({{f}}^{-1}\circ {K}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)$
41 fveq2 ${⊢}{n}={m}\to {f}\left({n}\right)={f}\left({m}\right)$
42 41 csbeq1d
43 elfznn ${⊢}{m}\in \left(1\dots {M}\right)\to {m}\in ℕ$
44 43 adantl ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {M}\right)\right)\to {m}\in ℕ$
45 f1of ${⊢}{f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}\to {f}:\left(1\dots {M}\right)⟶{A}$
46 6 45 syl ${⊢}{\phi }\to {f}:\left(1\dots {M}\right)⟶{A}$
47 46 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {M}\right)\right)\to {f}\left({m}\right)\in {A}$
48 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
49 48 adantr ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {M}\right)\right)\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
50 nfcsb1v
51 50 nfel1
52 csbeq1a
53 52 eleq1d
54 51 53 rspc
55 47 49 54 sylc
56 3 42 44 55 fvmptd3
57 56 55 eqeltrd ${⊢}\left({\phi }\wedge {m}\in \left(1\dots {M}\right)\right)\to {G}\left({m}\right)\in ℂ$
58 38 f1oeq2d ${⊢}{\phi }\to \left({K}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}↔{K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}\right)$
59 7 58 mpbird ${⊢}{\phi }\to {K}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}$
60 f1of ${⊢}{K}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}\to {K}:\left(1\dots {M}\right)⟶{A}$
61 59 60 syl ${⊢}{\phi }\to {K}:\left(1\dots {M}\right)⟶{A}$
62 fvco3 ${⊢}\left({K}:\left(1\dots {M}\right)⟶{A}\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({{f}}^{-1}\circ {K}\right)\left({i}\right)={{f}}^{-1}\left({K}\left({i}\right)\right)$
63 61 62 sylan ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({{f}}^{-1}\circ {K}\right)\left({i}\right)={{f}}^{-1}\left({K}\left({i}\right)\right)$
64 63 fveq2d ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {f}\left(\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\right)={f}\left({{f}}^{-1}\left({K}\left({i}\right)\right)\right)$
65 6 adantr ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}$
66 61 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {K}\left({i}\right)\in {A}$
67 f1ocnvfv2 ${⊢}\left({f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}\wedge {K}\left({i}\right)\in {A}\right)\to {f}\left({{f}}^{-1}\left({K}\left({i}\right)\right)\right)={K}\left({i}\right)$
68 65 66 67 syl2anc ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {f}\left({{f}}^{-1}\left({K}\left({i}\right)\right)\right)={K}\left({i}\right)$
69 64 68 eqtr2d ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {K}\left({i}\right)={f}\left(\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\right)$
70 69 csbeq1d
71 70 fveq2d
72 elfznn ${⊢}{i}\in \left(1\dots {M}\right)\to {i}\in ℕ$
73 72 adantl ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {i}\in ℕ$
74 fveq2 ${⊢}{n}={i}\to {K}\left({n}\right)={K}\left({i}\right)$
75 74 csbeq1d
76 75 4 fvmpti
77 73 76 syl
78 f1of ${⊢}\left({{f}}^{-1}\circ {K}\right):\left(1\dots {M}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}\right)\to \left({{f}}^{-1}\circ {K}\right):\left(1\dots {M}\right)⟶\left(1\dots {M}\right)$
79 40 78 syl ${⊢}{\phi }\to \left({{f}}^{-1}\circ {K}\right):\left(1\dots {M}\right)⟶\left(1\dots {M}\right)$
80 79 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to \left({{f}}^{-1}\circ {K}\right)\left({i}\right)\in \left(1\dots {M}\right)$
81 elfznn ${⊢}\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\in \left(1\dots {M}\right)\to \left({{f}}^{-1}\circ {K}\right)\left({i}\right)\in ℕ$
82 fveq2 ${⊢}{n}=\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\to {f}\left({n}\right)={f}\left(\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\right)$
83 82 csbeq1d
84 83 3 fvmpti
85 80 81 84 3syl
86 71 77 85 3eqtr4d ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {H}\left({i}\right)={G}\left(\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\right)$
87 9 11 13 16 17 40 57 86 seqf1o ${⊢}{\phi }\to seq1\left(+,{H}\right)\left({M}\right)=seq1\left(+,{G}\right)\left({M}\right)$
88 37 fveq2d ${⊢}{\phi }\to seq1\left(+,{H}\right)\left({M}\right)=seq1\left(+,{H}\right)\left({N}\right)$
89 87 88 eqtr3d ${⊢}{\phi }\to seq1\left(+,{G}\right)\left({M}\right)=seq1\left(+,{H}\right)\left({N}\right)$