Metamath Proof Explorer


Theorem prodmolem3

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

Ref Expression
Hypotheses prodmo.1 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) )
prodmo.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
prodmo.3 𝐺 = ( 𝑗 ∈ ℕ ↦ ( 𝑓𝑗 ) / 𝑘 𝐵 )
prodmolem3.4 𝐻 = ( 𝑗 ∈ ℕ ↦ ( 𝐾𝑗 ) / 𝑘 𝐵 )
prodmolem3.5 ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
prodmolem3.6 ( 𝜑𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 )
prodmolem3.7 ( 𝜑𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 )
Assertion prodmolem3 ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) )
2 prodmo.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
3 prodmo.3 𝐺 = ( 𝑗 ∈ ℕ ↦ ( 𝑓𝑗 ) / 𝑘 𝐵 )
4 prodmolem3.4 𝐻 = ( 𝑗 ∈ ℕ ↦ ( 𝐾𝑗 ) / 𝑘 𝐵 )
5 prodmolem3.5 ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
6 prodmolem3.6 ( 𝜑𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 )
7 prodmolem3.7 ( 𝜑𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 )
8 mulcl ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 · 𝑗 ) ∈ ℂ )
9 8 adantl ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 · 𝑗 ) ∈ ℂ )
10 mulcom ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 · 𝑗 ) = ( 𝑗 · 𝑚 ) )
11 10 adantl ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 · 𝑗 ) = ( 𝑗 · 𝑚 ) )
12 mulass ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑚 · 𝑗 ) · 𝑧 ) = ( 𝑚 · ( 𝑗 · 𝑧 ) ) )
13 12 adantl ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑚 · 𝑗 ) · 𝑧 ) = ( 𝑚 · ( 𝑗 · 𝑧 ) ) )
14 5 simpld ( 𝜑𝑀 ∈ ℕ )
15 nnuz ℕ = ( ℤ ‘ 1 )
16 14 15 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 1 ) )
17 ssidd ( 𝜑 → ℂ ⊆ ℂ )
18 f1ocnv ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 𝑓 : 𝐴1-1-onto→ ( 1 ... 𝑀 ) )
19 6 18 syl ( 𝜑 𝑓 : 𝐴1-1-onto→ ( 1 ... 𝑀 ) )
20 f1oco ( ( 𝑓 : 𝐴1-1-onto→ ( 1 ... 𝑀 ) ∧ 𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 ) → ( 𝑓𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) )
21 19 7 20 syl2anc ( 𝜑 → ( 𝑓𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) )
22 ovex ( 1 ... 𝑁 ) ∈ V
23 22 f1oen ( ( 𝑓𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) )
24 21 23 syl ( 𝜑 → ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) )
25 fzfi ( 1 ... 𝑁 ) ∈ Fin
26 fzfi ( 1 ... 𝑀 ) ∈ Fin
27 hashen ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 1 ... 𝑀 ) ∈ Fin ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) ) )
28 25 26 27 mp2an ( ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) )
29 24 28 sylibr ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) )
30 5 simprd ( 𝜑𝑁 ∈ ℕ )
31 30 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
32 hashfz1 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
33 31 32 syl ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
34 14 nnnn0d ( 𝜑𝑀 ∈ ℕ0 )
35 hashfz1 ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
36 34 35 syl ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
37 29 33 36 3eqtr3rd ( 𝜑𝑀 = 𝑁 )
38 37 oveq2d ( 𝜑 → ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) )
39 38 f1oeq2d ( 𝜑 → ( ( 𝑓𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ↔ ( 𝑓𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) ) )
40 21 39 mpbird ( 𝜑 → ( 𝑓𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
41 fveq2 ( 𝑗 = 𝑚 → ( 𝑓𝑗 ) = ( 𝑓𝑚 ) )
42 41 csbeq1d ( 𝑗 = 𝑚 ( 𝑓𝑗 ) / 𝑘 𝐵 = ( 𝑓𝑚 ) / 𝑘 𝐵 )
43 elfznn ( 𝑚 ∈ ( 1 ... 𝑀 ) → 𝑚 ∈ ℕ )
44 43 adantl ( ( 𝜑𝑚 ∈ ( 1 ... 𝑀 ) ) → 𝑚 ∈ ℕ )
45 f1of ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
46 6 45 syl ( 𝜑𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
47 46 ffvelrnda ( ( 𝜑𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓𝑚 ) ∈ 𝐴 )
48 2 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝐵 ∈ ℂ )
49 48 adantr ( ( 𝜑𝑚 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑘𝐴 𝐵 ∈ ℂ )
50 nfcsb1v 𝑘 ( 𝑓𝑚 ) / 𝑘 𝐵
51 50 nfel1 𝑘 ( 𝑓𝑚 ) / 𝑘 𝐵 ∈ ℂ
52 csbeq1a ( 𝑘 = ( 𝑓𝑚 ) → 𝐵 = ( 𝑓𝑚 ) / 𝑘 𝐵 )
53 52 eleq1d ( 𝑘 = ( 𝑓𝑚 ) → ( 𝐵 ∈ ℂ ↔ ( 𝑓𝑚 ) / 𝑘 𝐵 ∈ ℂ ) )
54 51 53 rspc ( ( 𝑓𝑚 ) ∈ 𝐴 → ( ∀ 𝑘𝐴 𝐵 ∈ ℂ → ( 𝑓𝑚 ) / 𝑘 𝐵 ∈ ℂ ) )
55 47 49 54 sylc ( ( 𝜑𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓𝑚 ) / 𝑘 𝐵 ∈ ℂ )
56 3 42 44 55 fvmptd3 ( ( 𝜑𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑚 ) = ( 𝑓𝑚 ) / 𝑘 𝐵 )
57 56 55 eqeltrd ( ( 𝜑𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑚 ) ∈ ℂ )
58 38 f1oeq2d ( 𝜑 → ( 𝐾 : ( 1 ... 𝑀 ) –1-1-onto𝐴𝐾 : ( 1 ... 𝑁 ) –1-1-onto𝐴 ) )
59 7 58 mpbird ( 𝜑𝐾 : ( 1 ... 𝑀 ) –1-1-onto𝐴 )
60 f1of ( 𝐾 : ( 1 ... 𝑀 ) –1-1-onto𝐴𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
61 59 60 syl ( 𝜑𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
62 fvco3 ( ( 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑓𝐾 ) ‘ 𝑖 ) = ( 𝑓 ‘ ( 𝐾𝑖 ) ) )
63 61 62 sylan ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑓𝐾 ) ‘ 𝑖 ) = ( 𝑓 ‘ ( 𝐾𝑖 ) ) )
64 63 fveq2d ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) = ( 𝑓 ‘ ( 𝑓 ‘ ( 𝐾𝑖 ) ) ) )
65 6 adantr ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 )
66 61 ffvelrnda ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐾𝑖 ) ∈ 𝐴 )
67 f1ocnvfv2 ( ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( 𝐾𝑖 ) ∈ 𝐴 ) → ( 𝑓 ‘ ( 𝑓 ‘ ( 𝐾𝑖 ) ) ) = ( 𝐾𝑖 ) )
68 65 66 67 syl2anc ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( 𝑓 ‘ ( 𝐾𝑖 ) ) ) = ( 𝐾𝑖 ) )
69 64 68 eqtrd ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) = ( 𝐾𝑖 ) )
70 69 csbeq1d ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) / 𝑘 𝐵 = ( 𝐾𝑖 ) / 𝑘 𝐵 )
71 70 fveq2d ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( I ‘ ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) / 𝑘 𝐵 ) = ( I ‘ ( 𝐾𝑖 ) / 𝑘 𝐵 ) )
72 f1of ( ( 𝑓𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( 𝑓𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
73 40 72 syl ( 𝜑 → ( 𝑓𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
74 73 ffvelrnda ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑓𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) )
75 elfznn ( ( ( 𝑓𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) → ( ( 𝑓𝐾 ) ‘ 𝑖 ) ∈ ℕ )
76 fveq2 ( 𝑗 = ( ( 𝑓𝐾 ) ‘ 𝑖 ) → ( 𝑓𝑗 ) = ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) )
77 76 csbeq1d ( 𝑗 = ( ( 𝑓𝐾 ) ‘ 𝑖 ) → ( 𝑓𝑗 ) / 𝑘 𝐵 = ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) / 𝑘 𝐵 )
78 77 3 fvmpti ( ( ( 𝑓𝐾 ) ‘ 𝑖 ) ∈ ℕ → ( 𝐺 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) / 𝑘 𝐵 ) )
79 74 75 78 3syl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ( 𝑓 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) / 𝑘 𝐵 ) )
80 elfznn ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℕ )
81 80 adantl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ℕ )
82 fveq2 ( 𝑗 = 𝑖 → ( 𝐾𝑗 ) = ( 𝐾𝑖 ) )
83 82 csbeq1d ( 𝑗 = 𝑖 ( 𝐾𝑗 ) / 𝑘 𝐵 = ( 𝐾𝑖 ) / 𝑘 𝐵 )
84 83 4 fvmpti ( 𝑖 ∈ ℕ → ( 𝐻𝑖 ) = ( I ‘ ( 𝐾𝑖 ) / 𝑘 𝐵 ) )
85 81 84 syl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻𝑖 ) = ( I ‘ ( 𝐾𝑖 ) / 𝑘 𝐵 ) )
86 71 79 85 3eqtr4rd ( ( 𝜑𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻𝑖 ) = ( 𝐺 ‘ ( ( 𝑓𝐾 ) ‘ 𝑖 ) ) )
87 9 11 13 16 17 40 57 86 seqf1o ( 𝜑 → ( seq 1 ( · , 𝐻 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
88 37 fveq2d ( 𝜑 → ( seq 1 ( · , 𝐻 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )
89 87 88 eqtr3d ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )