# Metamath Proof Explorer

## Theorem prodmolem2a

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
prodmolem2.4
prodmolem2.5 ${⊢}{\phi }\to {N}\in ℕ$
prodmolem2.6 ${⊢}{\phi }\to {M}\in ℤ$
prodmolem2.7 ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
prodmolem2.8 ${⊢}{\phi }\to {f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
prodmolem2.9 ${⊢}{\phi }\to {K}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
Assertion prodmolem2a ${⊢}{\phi }\to seq{M}\left(×,{F}\right)⇝seq1\left(×,{G}\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 prodmolem2.4
5 prodmolem2.5 ${⊢}{\phi }\to {N}\in ℕ$
6 prodmolem2.6 ${⊢}{\phi }\to {M}\in ℤ$
7 prodmolem2.7 ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
8 prodmolem2.8 ${⊢}{\phi }\to {f}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
9 prodmolem2.9 ${⊢}{\phi }\to {K}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)$
10 fzfid ${⊢}{\phi }\to \left(1\dots {N}\right)\in \mathrm{Fin}$
11 10 8 hasheqf1od ${⊢}{\phi }\to \left|\left(1\dots {N}\right)\right|=\left|{A}\right|$
12 5 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
13 hashfz1 ${⊢}{N}\in {ℕ}_{0}\to \left|\left(1\dots {N}\right)\right|={N}$
14 12 13 syl ${⊢}{\phi }\to \left|\left(1\dots {N}\right)\right|={N}$
15 11 14 eqtr3d ${⊢}{\phi }\to \left|{A}\right|={N}$
16 15 oveq2d ${⊢}{\phi }\to \left(1\dots \left|{A}\right|\right)=\left(1\dots {N}\right)$
17 isoeq4 ${⊢}\left(1\dots \left|{A}\right|\right)=\left(1\dots {N}\right)\to \left({K}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)↔{K}{Isom}_{<,<}\left(\left(1\dots {N}\right),{A}\right)\right)$
18 16 17 syl ${⊢}{\phi }\to \left({K}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)↔{K}{Isom}_{<,<}\left(\left(1\dots {N}\right),{A}\right)\right)$
19 9 18 mpbid ${⊢}{\phi }\to {K}{Isom}_{<,<}\left(\left(1\dots {N}\right),{A}\right)$
20 isof1o ${⊢}{K}{Isom}_{<,<}\left(\left(1\dots {N}\right),{A}\right)\to {K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
21 f1of ${⊢}{K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}\to {K}:\left(1\dots {N}\right)⟶{A}$
22 19 20 21 3syl ${⊢}{\phi }\to {K}:\left(1\dots {N}\right)⟶{A}$
23 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
24 5 23 eleqtrdi ${⊢}{\phi }\to {N}\in {ℤ}_{\ge 1}$
25 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge 1}\to {N}\in \left(1\dots {N}\right)$
26 24 25 syl ${⊢}{\phi }\to {N}\in \left(1\dots {N}\right)$
27 22 26 ffvelrnd ${⊢}{\phi }\to {K}\left({N}\right)\in {A}$
28 7 27 sseldd ${⊢}{\phi }\to {K}\left({N}\right)\in {ℤ}_{\ge {M}}$
29 7 sselda ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {j}\in {ℤ}_{\ge {M}}$
30 19 20 syl ${⊢}{\phi }\to {K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}$
31 f1ocnvfv2 ${⊢}\left({K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}\wedge {j}\in {A}\right)\to {K}\left({{K}}^{-1}\left({j}\right)\right)={j}$
32 30 31 sylan ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {K}\left({{K}}^{-1}\left({j}\right)\right)={j}$
33 f1ocnv ${⊢}{K}:\left(1\dots {N}\right)\underset{1-1 onto}{⟶}{A}\to {{K}}^{-1}:{A}\underset{1-1 onto}{⟶}\left(1\dots {N}\right)$
34 f1of ${⊢}{{K}}^{-1}:{A}\underset{1-1 onto}{⟶}\left(1\dots {N}\right)\to {{K}}^{-1}:{A}⟶\left(1\dots {N}\right)$
35 30 33 34 3syl ${⊢}{\phi }\to {{K}}^{-1}:{A}⟶\left(1\dots {N}\right)$
36 35 ffvelrnda ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {{K}}^{-1}\left({j}\right)\in \left(1\dots {N}\right)$
37 elfzle2 ${⊢}{{K}}^{-1}\left({j}\right)\in \left(1\dots {N}\right)\to {{K}}^{-1}\left({j}\right)\le {N}$
38 36 37 syl ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {{K}}^{-1}\left({j}\right)\le {N}$
39 19 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {K}{Isom}_{<,<}\left(\left(1\dots {N}\right),{A}\right)$
40 fzssuz ${⊢}\left(1\dots {N}\right)\subseteq {ℤ}_{\ge 1}$
41 uzssz ${⊢}{ℤ}_{\ge 1}\subseteq ℤ$
42 zssre ${⊢}ℤ\subseteq ℝ$
43 41 42 sstri ${⊢}{ℤ}_{\ge 1}\subseteq ℝ$
44 40 43 sstri ${⊢}\left(1\dots {N}\right)\subseteq ℝ$
45 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
46 44 45 sstri ${⊢}\left(1\dots {N}\right)\subseteq {ℝ}^{*}$
47 46 a1i ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left(1\dots {N}\right)\subseteq {ℝ}^{*}$
48 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
49 48 42 sstri ${⊢}{ℤ}_{\ge {M}}\subseteq ℝ$
50 49 45 sstri ${⊢}{ℤ}_{\ge {M}}\subseteq {ℝ}^{*}$
51 7 50 sstrdi ${⊢}{\phi }\to {A}\subseteq {ℝ}^{*}$
52 51 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {A}\subseteq {ℝ}^{*}$
53 26 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {N}\in \left(1\dots {N}\right)$
54 leisorel ${⊢}\left({K}{Isom}_{<,<}\left(\left(1\dots {N}\right),{A}\right)\wedge \left(\left(1\dots {N}\right)\subseteq {ℝ}^{*}\wedge {A}\subseteq {ℝ}^{*}\right)\wedge \left({{K}}^{-1}\left({j}\right)\in \left(1\dots {N}\right)\wedge {N}\in \left(1\dots {N}\right)\right)\right)\to \left({{K}}^{-1}\left({j}\right)\le {N}↔{K}\left({{K}}^{-1}\left({j}\right)\right)\le {K}\left({N}\right)\right)$
55 39 47 52 36 53 54 syl122anc ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left({{K}}^{-1}\left({j}\right)\le {N}↔{K}\left({{K}}^{-1}\left({j}\right)\right)\le {K}\left({N}\right)\right)$
56 38 55 mpbid ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {K}\left({{K}}^{-1}\left({j}\right)\right)\le {K}\left({N}\right)$
57 32 56 eqbrtrrd ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {j}\le {K}\left({N}\right)$
58 7 48 sstrdi ${⊢}{\phi }\to {A}\subseteq ℤ$
59 58 sselda ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {j}\in ℤ$
60 eluzelz ${⊢}{K}\left({N}\right)\in {ℤ}_{\ge {M}}\to {K}\left({N}\right)\in ℤ$
61 28 60 syl ${⊢}{\phi }\to {K}\left({N}\right)\in ℤ$
62 61 adantr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {K}\left({N}\right)\in ℤ$
63 eluz ${⊢}\left({j}\in ℤ\wedge {K}\left({N}\right)\in ℤ\right)\to \left({K}\left({N}\right)\in {ℤ}_{\ge {j}}↔{j}\le {K}\left({N}\right)\right)$
64 59 62 63 syl2anc ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left({K}\left({N}\right)\in {ℤ}_{\ge {j}}↔{j}\le {K}\left({N}\right)\right)$
65 57 64 mpbird ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {K}\left({N}\right)\in {ℤ}_{\ge {j}}$
66 elfzuzb ${⊢}{j}\in \left({M}\dots {K}\left({N}\right)\right)↔\left({j}\in {ℤ}_{\ge {M}}\wedge {K}\left({N}\right)\in {ℤ}_{\ge {j}}\right)$
67 29 65 66 sylanbrc ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {j}\in \left({M}\dots {K}\left({N}\right)\right)$
68 67 ex ${⊢}{\phi }\to \left({j}\in {A}\to {j}\in \left({M}\dots {K}\left({N}\right)\right)\right)$
69 68 ssrdv ${⊢}{\phi }\to {A}\subseteq \left({M}\dots {K}\left({N}\right)\right)$
70 1 2 28 69 fprodcvg ${⊢}{\phi }\to seq{M}\left(×,{F}\right)⇝seq{M}\left(×,{F}\right)\left({K}\left({N}\right)\right)$
71 mulid2 ${⊢}{m}\in ℂ\to 1{m}={m}$
72 71 adantl ${⊢}\left({\phi }\wedge {m}\in ℂ\right)\to 1{m}={m}$
73 mulid1 ${⊢}{m}\in ℂ\to {m}\cdot 1={m}$
74 73 adantl ${⊢}\left({\phi }\wedge {m}\in ℂ\right)\to {m}\cdot 1={m}$
75 mulcl ${⊢}\left({m}\in ℂ\wedge {x}\in ℂ\right)\to {m}{x}\in ℂ$
76 75 adantl ${⊢}\left({\phi }\wedge \left({m}\in ℂ\wedge {x}\in ℂ\right)\right)\to {m}{x}\in ℂ$
77 1cnd ${⊢}{\phi }\to 1\in ℂ$
78 26 16 eleqtrrd ${⊢}{\phi }\to {N}\in \left(1\dots \left|{A}\right|\right)$
79 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{B},1\right)={B}$
80 79 adantl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},1\right)={B}$
81 80 2 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
82 81 ex ${⊢}{\phi }\to \left({k}\in {A}\to if\left({k}\in {A},{B},1\right)\in ℂ\right)$
83 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},1\right)=1$
84 ax-1cn ${⊢}1\in ℂ$
85 83 84 eqeltrdi ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},1\right)\in ℂ$
86 82 85 pm2.61d1 ${⊢}{\phi }\to if\left({k}\in {A},{B},1\right)\in ℂ$
87 86 adantr ${⊢}\left({\phi }\wedge {k}\in ℤ\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
88 87 1 fmptd ${⊢}{\phi }\to {F}:ℤ⟶ℂ$
89 elfzelz ${⊢}{m}\in \left({M}\dots {K}\left(\left|{A}\right|\right)\right)\to {m}\in ℤ$
90 ffvelrn ${⊢}\left({F}:ℤ⟶ℂ\wedge {m}\in ℤ\right)\to {F}\left({m}\right)\in ℂ$
91 88 89 90 syl2an ${⊢}\left({\phi }\wedge {m}\in \left({M}\dots {K}\left(\left|{A}\right|\right)\right)\right)\to {F}\left({m}\right)\in ℂ$
92 fveqeq2 ${⊢}{k}={m}\to \left({F}\left({k}\right)=1↔{F}\left({m}\right)=1\right)$
93 fzssz ${⊢}\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\subseteq ℤ$
94 eldifi ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to {k}\in \left({M}\dots {K}\left(\left|{A}\right|\right)\right)$
95 93 94 sseldi ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to {k}\in ℤ$
96 eldifn ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to ¬{k}\in {A}$
97 96 83 syl ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to if\left({k}\in {A},{B},1\right)=1$
98 97 84 eqeltrdi ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
99 1 fvmpt2 ${⊢}\left({k}\in ℤ\wedge if\left({k}\in {A},{B},1\right)\in ℂ\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
100 95 98 99 syl2anc ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
101 100 97 eqtrd ${⊢}{k}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to {F}\left({k}\right)=1$
102 92 101 vtoclga ${⊢}{m}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\to {F}\left({m}\right)=1$
103 102 adantl ${⊢}\left({\phi }\wedge {m}\in \left(\left({M}\dots {K}\left(\left|{A}\right|\right)\right)\setminus {A}\right)\right)\to {F}\left({m}\right)=1$
104 isof1o ${⊢}{K}{Isom}_{<,<}\left(\left(1\dots \left|{A}\right|\right),{A}\right)\to {K}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}$
105 f1of ${⊢}{K}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to {K}:\left(1\dots \left|{A}\right|\right)⟶{A}$
106 9 104 105 3syl ${⊢}{\phi }\to {K}:\left(1\dots \left|{A}\right|\right)⟶{A}$
107 106 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to {K}\left({x}\right)\in {A}$
108 107 iftrued
109 58 adantr ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to {A}\subseteq ℤ$
110 109 107 sseldd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to {K}\left({x}\right)\in ℤ$
111 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
112 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{K}\left({x}\right)\in {A}$
113 nfcsb1v
114 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}1$
115 112 113 114 nfif
116 115 nfel1
117 111 116 nfim
118 fvex ${⊢}{K}\left({x}\right)\in \mathrm{V}$
119 eleq1 ${⊢}{k}={K}\left({x}\right)\to \left({k}\in {A}↔{K}\left({x}\right)\in {A}\right)$
120 csbeq1a
121 119 120 ifbieq1d
122 121 eleq1d
123 122 imbi2d
124 117 118 123 86 vtoclf
126 eleq1 ${⊢}{n}={K}\left({x}\right)\to \left({n}\in {A}↔{K}\left({x}\right)\in {A}\right)$
127 csbeq1
128 126 127 ifbieq1d
129 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)$
130 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{n}\in {A}$
131 nfcsb1v
132 130 131 114 nfif
133 eleq1 ${⊢}{k}={n}\to \left({k}\in {A}↔{n}\in {A}\right)$
134 csbeq1a
135 133 134 ifbieq1d
136 129 132 135 cbvmpt
137 1 136 eqtri
138 128 137 fvmptg
139 110 125 138 syl2anc
140 elfznn ${⊢}{x}\in \left(1\dots \left|{A}\right|\right)\to {x}\in ℕ$
141 108 125 eqeltrrd
142 fveq2 ${⊢}{j}={x}\to {K}\left({j}\right)={K}\left({x}\right)$
143 142 csbeq1d
144 143 4 fvmptg
145 140 141 144 syl2an2
146 108 139 145 3eqtr4rd ${⊢}\left({\phi }\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to {H}\left({x}\right)={F}\left({K}\left({x}\right)\right)$
147 72 74 76 77 9 78 7 91 103 146 seqcoll ${⊢}{\phi }\to seq{M}\left(×,{F}\right)\left({K}\left({N}\right)\right)=seq1\left(×,{H}\right)\left({N}\right)$
148 5 5 jca ${⊢}{\phi }\to \left({N}\in ℕ\wedge {N}\in ℕ\right)$
149 1 2 3 4 148 8 30 prodmolem3 ${⊢}{\phi }\to seq1\left(×,{G}\right)\left({N}\right)=seq1\left(×,{H}\right)\left({N}\right)$
150 147 149 eqtr4d ${⊢}{\phi }\to seq{M}\left(×,{F}\right)\left({K}\left({N}\right)\right)=seq1\left(×,{G}\right)\left({N}\right)$
151 70 150 breqtrd ${⊢}{\phi }\to seq{M}\left(×,{F}\right)⇝seq1\left(×,{G}\right)\left({N}\right)$