Metamath Proof Explorer


Theorem ulmss

Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses ulmss.z 𝑍 = ( ℤ𝑀 )
ulmss.t ( 𝜑𝑇𝑆 )
ulmss.a ( ( 𝜑𝑥𝑍 ) → 𝐴𝑊 )
ulmss.u ( 𝜑 → ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺 )
Assertion ulmss ( 𝜑 → ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ( ⇝𝑢𝑇 ) ( 𝐺𝑇 ) )

Proof

Step Hyp Ref Expression
1 ulmss.z 𝑍 = ( ℤ𝑀 )
2 ulmss.t ( 𝜑𝑇𝑆 )
3 ulmss.a ( ( 𝜑𝑥𝑍 ) → 𝐴𝑊 )
4 ulmss.u ( 𝜑 → ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺 )
5 1 uztrn2 ( ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
6 2 adantr ( ( 𝜑𝑘𝑍 ) → 𝑇𝑆 )
7 ssralv ( 𝑇𝑆 → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
8 6 7 syl ( ( 𝜑𝑘𝑍 ) → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
9 fvres ( 𝑧𝑇 → ( ( 𝐴𝑇 ) ‘ 𝑧 ) = ( 𝐴𝑧 ) )
10 9 ad2antll ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( ( 𝐴𝑇 ) ‘ 𝑧 ) = ( 𝐴𝑧 ) )
11 simprl ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → 𝑥𝑍 )
12 3 adantrr ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → 𝐴𝑊 )
13 12 resexd ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( 𝐴𝑇 ) ∈ V )
14 eqid ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) = ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) )
15 14 fvmpt2 ( ( 𝑥𝑍 ∧ ( 𝐴𝑇 ) ∈ V ) → ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) = ( 𝐴𝑇 ) )
16 11 13 15 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) = ( 𝐴𝑇 ) )
17 16 fveq1d ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( 𝐴𝑇 ) ‘ 𝑧 ) )
18 eqid ( 𝑥𝑍𝐴 ) = ( 𝑥𝑍𝐴 )
19 18 fvmpt2 ( ( 𝑥𝑍𝐴𝑊 ) → ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) = 𝐴 )
20 11 12 19 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) = 𝐴 )
21 20 fveq1d ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) = ( 𝐴𝑧 ) )
22 10 17 21 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑍𝑧𝑇 ) ) → ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) )
23 22 ralrimivva ( 𝜑 → ∀ 𝑥𝑍𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) )
24 nfv 𝑘𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 )
25 nfcv 𝑥 𝑇
26 nffvmpt1 𝑥 ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 )
27 nfcv 𝑥 𝑧
28 26 27 nffv 𝑥 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 )
29 nffvmpt1 𝑥 ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 )
30 29 27 nffv 𝑥 ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 )
31 28 30 nfeq 𝑥 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 )
32 25 31 nfralw 𝑥𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 )
33 fveq2 ( 𝑥 = 𝑘 → ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) = ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) )
34 33 fveq1d ( 𝑥 = 𝑘 → ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) )
35 fveq2 ( 𝑥 = 𝑘 → ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) = ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) )
36 35 fveq1d ( 𝑥 = 𝑘 → ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
37 34 36 eqeq12d ( 𝑥 = 𝑘 → ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) ↔ ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) ) )
38 37 ralbidv ( 𝑥 = 𝑘 → ( ∀ 𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) ↔ ∀ 𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) ) )
39 24 32 38 cbvralw ( ∀ 𝑥𝑍𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑥 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑥 ) ‘ 𝑧 ) ↔ ∀ 𝑘𝑍𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
40 23 39 sylib ( 𝜑 → ∀ 𝑘𝑍𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
41 40 r19.21bi ( ( 𝜑𝑘𝑍 ) → ∀ 𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
42 fvoveq1 ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) → ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) = ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) )
43 42 breq1d ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) → ( ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
44 43 ralimi ( ∀ 𝑧𝑇 ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) → ∀ 𝑧𝑇 ( ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
45 ralbi ( ∀ 𝑧𝑇 ( ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) → ( ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
46 41 44 45 3syl ( ( 𝜑𝑘𝑍 ) → ( ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ↔ ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
47 8 46 sylibrd ( ( 𝜑𝑘𝑍 ) → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
48 5 47 sylan2 ( ( 𝜑 ∧ ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) ) → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
49 48 anassrs ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
50 49 ralimdva ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
51 50 reximdva ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
52 51 ralimdv ( 𝜑 → ( ∀ 𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 → ∀ 𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
53 ulmf ( ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺 → ∃ 𝑚 ∈ ℤ ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) )
54 4 53 syl ( 𝜑 → ∃ 𝑚 ∈ ℤ ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) )
55 fdm ( ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → dom ( 𝑥𝑍𝐴 ) = ( ℤ𝑚 ) )
56 18 dmmptss dom ( 𝑥𝑍𝐴 ) ⊆ 𝑍
57 55 56 eqsstrrdi ( ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → ( ℤ𝑚 ) ⊆ 𝑍 )
58 uzid ( 𝑚 ∈ ℤ → 𝑚 ∈ ( ℤ𝑚 ) )
59 58 adantl ( ( 𝜑𝑚 ∈ ℤ ) → 𝑚 ∈ ( ℤ𝑚 ) )
60 ssel ( ( ℤ𝑚 ) ⊆ 𝑍 → ( 𝑚 ∈ ( ℤ𝑚 ) → 𝑚𝑍 ) )
61 eluzel2 ( 𝑚 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
62 61 1 eleq2s ( 𝑚𝑍𝑀 ∈ ℤ )
63 60 62 syl6 ( ( ℤ𝑚 ) ⊆ 𝑍 → ( 𝑚 ∈ ( ℤ𝑚 ) → 𝑀 ∈ ℤ ) )
64 57 59 63 syl2imc ( ( 𝜑𝑚 ∈ ℤ ) → ( ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝑀 ∈ ℤ ) )
65 64 rexlimdva ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → 𝑀 ∈ ℤ ) )
66 54 65 mpd ( 𝜑𝑀 ∈ ℤ )
67 3 ralrimiva ( 𝜑 → ∀ 𝑥𝑍 𝐴𝑊 )
68 18 fnmpt ( ∀ 𝑥𝑍 𝐴𝑊 → ( 𝑥𝑍𝐴 ) Fn 𝑍 )
69 67 68 syl ( 𝜑 → ( 𝑥𝑍𝐴 ) Fn 𝑍 )
70 frn ( ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → ran ( 𝑥𝑍𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) )
71 70 rexlimivw ( ∃ 𝑚 ∈ ℤ ( 𝑥𝑍𝐴 ) : ( ℤ𝑚 ) ⟶ ( ℂ ↑m 𝑆 ) → ran ( 𝑥𝑍𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) )
72 54 71 syl ( 𝜑 → ran ( 𝑥𝑍𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) )
73 df-f ( ( 𝑥𝑍𝐴 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ↔ ( ( 𝑥𝑍𝐴 ) Fn 𝑍 ∧ ran ( 𝑥𝑍𝐴 ) ⊆ ( ℂ ↑m 𝑆 ) ) )
74 69 72 73 sylanbrc ( 𝜑 → ( 𝑥𝑍𝐴 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
75 eqidd ( ( 𝜑 ∧ ( 𝑘𝑍𝑧𝑆 ) ) → ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) )
76 eqidd ( ( 𝜑𝑧𝑆 ) → ( 𝐺𝑧 ) = ( 𝐺𝑧 ) )
77 ulmcl ( ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺𝐺 : 𝑆 ⟶ ℂ )
78 4 77 syl ( 𝜑𝐺 : 𝑆 ⟶ ℂ )
79 ulmscl ( ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺𝑆 ∈ V )
80 4 79 syl ( 𝜑𝑆 ∈ V )
81 1 66 74 75 76 78 80 ulm2 ( 𝜑 → ( ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺 ↔ ∀ 𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( ( 𝑥𝑍𝐴 ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
82 74 fvmptelrn ( ( 𝜑𝑥𝑍 ) → 𝐴 ∈ ( ℂ ↑m 𝑆 ) )
83 elmapi ( 𝐴 ∈ ( ℂ ↑m 𝑆 ) → 𝐴 : 𝑆 ⟶ ℂ )
84 82 83 syl ( ( 𝜑𝑥𝑍 ) → 𝐴 : 𝑆 ⟶ ℂ )
85 2 adantr ( ( 𝜑𝑥𝑍 ) → 𝑇𝑆 )
86 84 85 fssresd ( ( 𝜑𝑥𝑍 ) → ( 𝐴𝑇 ) : 𝑇 ⟶ ℂ )
87 cnex ℂ ∈ V
88 80 2 ssexd ( 𝜑𝑇 ∈ V )
89 88 adantr ( ( 𝜑𝑥𝑍 ) → 𝑇 ∈ V )
90 elmapg ( ( ℂ ∈ V ∧ 𝑇 ∈ V ) → ( ( 𝐴𝑇 ) ∈ ( ℂ ↑m 𝑇 ) ↔ ( 𝐴𝑇 ) : 𝑇 ⟶ ℂ ) )
91 87 89 90 sylancr ( ( 𝜑𝑥𝑍 ) → ( ( 𝐴𝑇 ) ∈ ( ℂ ↑m 𝑇 ) ↔ ( 𝐴𝑇 ) : 𝑇 ⟶ ℂ ) )
92 86 91 mpbird ( ( 𝜑𝑥𝑍 ) → ( 𝐴𝑇 ) ∈ ( ℂ ↑m 𝑇 ) )
93 92 fmpttd ( 𝜑 → ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑇 ) )
94 eqidd ( ( 𝜑 ∧ ( 𝑘𝑍𝑧𝑇 ) ) → ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) )
95 fvres ( 𝑧𝑇 → ( ( 𝐺𝑇 ) ‘ 𝑧 ) = ( 𝐺𝑧 ) )
96 95 adantl ( ( 𝜑𝑧𝑇 ) → ( ( 𝐺𝑇 ) ‘ 𝑧 ) = ( 𝐺𝑧 ) )
97 78 2 fssresd ( 𝜑 → ( 𝐺𝑇 ) : 𝑇 ⟶ ℂ )
98 1 66 93 94 96 97 88 ulm2 ( 𝜑 → ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ( ⇝𝑢𝑇 ) ( 𝐺𝑇 ) ↔ ∀ 𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑇 ( abs ‘ ( ( ( ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑟 ) )
99 52 81 98 3imtr4d ( 𝜑 → ( ( 𝑥𝑍𝐴 ) ( ⇝𝑢𝑆 ) 𝐺 → ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ( ⇝𝑢𝑇 ) ( 𝐺𝑇 ) ) )
100 4 99 mpd ( 𝜑 → ( 𝑥𝑍 ↦ ( 𝐴𝑇 ) ) ( ⇝𝑢𝑇 ) ( 𝐺𝑇 ) )