This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmshftlem

Description: Lemma for ulmshft . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmshft.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmshft.w ⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) )
ulmshft.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmshft.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
ulmshft.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulmshft.h ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) )
Assertion ulmshftlem ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ulmshft.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmshft.w ⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) )
3 ulmshft.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 ulmshft.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5 ulmshft.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
6 ulmshft.h ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) )
7 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
8 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
9 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
10 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
13 1 7 8 9 10 11 12 ulmi ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
14 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
15 14 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
16 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → 𝐾 ∈ ℤ )
17 eluzadd ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑖 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
18 15 16 17 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
19 18 2 eleqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 + 𝐾 ) ∈ 𝑊 )
20 eluzelz ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑖 ∈ ℤ )
21 15 20 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ℤ )
22 21 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ) → 𝑖 ∈ ℤ )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐾 ∈ ℤ )
24 23 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ) → 𝐾 ∈ ℤ )
25 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) )
26 eluzsub ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ) → ( 𝑘 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑖 ) )
27 22 24 25 26 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ) → ( 𝑘 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑖 ) )
28 fveq2 ⊢ ( 𝑚 = ( 𝑘 − 𝐾 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) )
29 28 fveq1d ⊢ ( 𝑚 = ( 𝑘 − 𝐾 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) )
30 29 fvoveq1d ⊢ ( 𝑚 = ( 𝑘 − 𝐾 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
31 30 breq1d ⊢ ( 𝑚 = ( 𝑘 − 𝐾 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
32 31 ralbidv ⊢ ( 𝑚 = ( 𝑘 − 𝐾 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
33 32 rspcv ⊢ ( ( 𝑘 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑖 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
34 27 33 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
35 34 ralrimdva ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
36 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 𝐾 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) )
37 36 raleqdv ⊢ ( 𝑗 = ( 𝑖 + 𝐾 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
38 37 rspcev ⊢ ( ( ( 𝑖 + 𝐾 ) ∈ 𝑊 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 𝐾 ) ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑊 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
39 19 35 38 syl6an ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑊 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
40 39 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑖 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑊 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
41 13 40 mpd ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑊 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
42 41 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑊 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 )
43 3 4 zaddcld ⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ℤ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → ( 𝑀 + 𝐾 ) ∈ ℤ )
45 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
46 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝑀 ∈ ℤ )
47 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝐾 ∈ ℤ )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝑛 ∈ 𝑊 )
49 48 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
50 eluzsub ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑛 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
51 46 47 49 50 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝑛 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
52 51 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝑛 − 𝐾 ) ∈ 𝑍 )
53 45 52 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ∈ ( ℂ ↑m 𝑆 ) )
54 6 53 fmpt3d ⊢ ( 𝜑 → 𝐻 : 𝑊 ⟶ ( ℂ ↑m 𝑆 ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐻 : 𝑊 ⟶ ( ℂ ↑m 𝑆 ) )
56 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ ( 𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆 ) ) → 𝐻 = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) )
57 56 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ ( 𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ 𝑘 ) )
58 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) = ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) )
59 eqid ⊢ ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) )
60 fvex ⊢ ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ∈ V
61 58 59 60 fvmpt ⊢ ( 𝑘 ∈ 𝑊 → ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) )
62 61 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ ( 𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) )
63 57 62 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ ( 𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) )
64 63 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ ( 𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐻 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) )
65 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
66 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐺 : 𝑆 ⟶ ℂ )
68 ulmscl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝑆 ∈ V )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝑆 ∈ V )
70 2 44 55 64 65 67 69 ulm2 ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → ( 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑊 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ ( 𝑘 − 𝐾 ) ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) )
71 42 70 mpbird ⊢ ( ( 𝜑 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
72 71 ex ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )