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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ∈ ( ℂ ↑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	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )