Metamath Proof Explorer

Theorem summolem3

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

Ref Expression
Hypotheses summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
summo.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
summolem3.4 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
summolem3.5 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
summolem3.6 ⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
summolem3.7 ⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
Assertion summolem3 ( 𝜑 → ( seq 1 ( + , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2 summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 summo.3 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
4 summolem3.4 ⊢ 𝐻 = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
5 summolem3.5 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
6 summolem3.6 ⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
7 summolem3.7 ⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
8 addcl ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 + 𝑗 ) ∈ ℂ )
9 8 adantl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 + 𝑗 ) ∈ ℂ )
10 addcom ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 + 𝑗 ) = ( 𝑗 + 𝑚 ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 + 𝑗 ) = ( 𝑗 + 𝑚 ) )
12 addass ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑚 + 𝑗 ) + 𝑦 ) = ( 𝑚 + ( 𝑗 + 𝑦 ) ) )
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 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
32 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
33 30 31 32 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
34 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
35 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
36 14 34 35 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝐴 )
67 f1ocnvfv2 ⊢ ( ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( 𝐾 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ 𝑖 ) )
68 65 66 67 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ 𝑖 ) )
69 64 68 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐾 ‘ 𝑖 ) = ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) )
70 69 csbeq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 )
71 70 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) )
72 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℕ )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ℕ )
74 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑖 ) )
75 74 csbeq1d ⊢ ( 𝑛 = 𝑖 → ⦋ ( 𝐾 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 )
76 75 4 fvmpti ⊢ ( 𝑖 ∈ ℕ → ( 𝐻 ‘ 𝑖 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) )
77 73 76 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑖 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) )
78 f1of ⊢ ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
79 40 78 syl ⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
80 79 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) )
81 elfznn ⊢ ( ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ℕ )
82 fveq2 ⊢ ( 𝑛 = ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) )
83 82 csbeq1d ⊢ ( 𝑛 = ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 )
84 83 3 fvmpti ⊢ ( ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ℕ → ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) )
85 80 81 84 3syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) )
86 71 77 85 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 ( + , 𝐻 ) ‘ 𝑁 ) )