# Metamath Proof Explorer

## Theorem prodmolem3

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

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

### Proof

Step Hyp Ref Expression
1 prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
2 prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 prodmo.3
4 prodmolem3.4
5 prodmolem3.5 ${⊢}{\phi }\to \left({M}\in ℕ\wedge {N}\in ℕ\right)$
6 prodmolem3.6 ${⊢}{\phi }\to {f}:\left(1\dots {M}\right)\underset{1-1 onto}{⟶}{A}$
7 prodmolem3.7 ${⊢}{\phi }\to {K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
8 mulcl ${⊢}\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 mulcom ${⊢}\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 mulass ${⊢}\left({m}\in ℂ\wedge {j}\in ℂ\wedge {z}\in ℂ\right)\to {m}{j}{z}={m}{j}{z}$
13 12 adantl ${⊢}\left({\phi }\wedge \left({m}\in ℂ\wedge {j}\in ℂ\wedge {z}\in ℂ\right)\right)\to {m}{j}{z}={m}{j}{z}$
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 30 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
32 hashfz1 ${⊢}{N}\in {ℕ}_{0}\to \left|\left(1\dots {N}\right)\right|={N}$
33 31 32 syl ${⊢}{\phi }\to \left|\left(1\dots {N}\right)\right|={N}$
34 14 nnnn0d ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
35 hashfz1 ${⊢}{M}\in {ℕ}_{0}\to \left|\left(1\dots {M}\right)\right|={M}$
36 34 35 syl ${⊢}{\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 ${⊢}{j}={m}\to {f}\left({j}\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 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {f}\left(\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\right)={K}\left({i}\right)$
70 69 csbeq1d
71 70 fveq2d
72 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)$
73 40 72 syl ${⊢}{\phi }\to \left({{f}}^{-1}\circ {K}\right):\left(1\dots {M}\right)⟶\left(1\dots {M}\right)$
74 73 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)$
75 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 ℕ$
76 fveq2 ${⊢}{j}=\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\to {f}\left({j}\right)={f}\left(\left({{f}}^{-1}\circ {K}\right)\left({i}\right)\right)$
77 76 csbeq1d
78 77 3 fvmpti
79 74 75 78 3syl
80 elfznn ${⊢}{i}\in \left(1\dots {M}\right)\to {i}\in ℕ$
81 80 adantl ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {i}\in ℕ$
82 fveq2 ${⊢}{j}={i}\to {K}\left({j}\right)={K}\left({i}\right)$
83 82 csbeq1d
84 83 4 fvmpti
85 81 84 syl
86 71 79 85 3eqtr4rd ${⊢}\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)$