MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ulmss Structured version   Visualization version   GIF version

Theorem ulmss 23869
Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015.)
Hypotheses
Ref Expression
ulmss.z 𝑍 = (ℤ𝑀)
ulmss.t (𝜑𝑇𝑆)
ulmss.a ((𝜑𝑥𝑍) → 𝐴𝑊)
ulmss.u (𝜑 → (𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺)
Assertion
Ref Expression
ulmss (𝜑 → (𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇))
Distinct variable groups:   𝑥,𝑇   𝜑,𝑥   𝑥,𝑆   𝑥,𝑍
Allowed substitution hints:   𝐴(𝑥)   𝐺(𝑥)   𝑀(𝑥)   𝑊(𝑥)

Proof of Theorem ulmss
Dummy variables 𝑗 𝑘 𝑚 𝑟 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ulmss.u . 2 (𝜑 → (𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺)
2 ulmss.z . . . . . . . . 9 𝑍 = (ℤ𝑀)
32uztrn2 11534 . . . . . . . 8 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
4 ulmss.t . . . . . . . . . . 11 (𝜑𝑇𝑆)
54adantr 479 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝑇𝑆)
6 ssralv 3625 . . . . . . . . . 10 (𝑇𝑆 → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
75, 6syl 17 . . . . . . . . 9 ((𝜑𝑘𝑍) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
8 fvres 6099 . . . . . . . . . . . . . . 15 (𝑧𝑇 → ((𝐴𝑇)‘𝑧) = (𝐴𝑧))
98ad2antll 760 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → ((𝐴𝑇)‘𝑧) = (𝐴𝑧))
10 simprl 789 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → 𝑥𝑍)
11 ulmss.a . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑍) → 𝐴𝑊)
1211adantrr 748 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → 𝐴𝑊)
13 resexg 5346 . . . . . . . . . . . . . . . . 17 (𝐴𝑊 → (𝐴𝑇) ∈ V)
1412, 13syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (𝐴𝑇) ∈ V)
15 eqid 2606 . . . . . . . . . . . . . . . . 17 (𝑥𝑍 ↦ (𝐴𝑇)) = (𝑥𝑍 ↦ (𝐴𝑇))
1615fvmpt2 6182 . . . . . . . . . . . . . . . 16 ((𝑥𝑍 ∧ (𝐴𝑇) ∈ V) → ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥) = (𝐴𝑇))
1710, 14, 16syl2anc 690 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥) = (𝐴𝑇))
1817fveq1d 6087 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = ((𝐴𝑇)‘𝑧))
19 eqid 2606 . . . . . . . . . . . . . . . . 17 (𝑥𝑍𝐴) = (𝑥𝑍𝐴)
2019fvmpt2 6182 . . . . . . . . . . . . . . . 16 ((𝑥𝑍𝐴𝑊) → ((𝑥𝑍𝐴)‘𝑥) = 𝐴)
2110, 12, 20syl2anc 690 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → ((𝑥𝑍𝐴)‘𝑥) = 𝐴)
2221fveq1d 6087 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (((𝑥𝑍𝐴)‘𝑥)‘𝑧) = (𝐴𝑧))
239, 18, 223eqtr4d 2650 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑍𝑧𝑇)) → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧))
2423ralrimivva 2950 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧))
25 nfv 1829 . . . . . . . . . . . . 13 𝑘𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧)
26 nfcv 2747 . . . . . . . . . . . . . 14 𝑥𝑇
27 nffvmpt1 6093 . . . . . . . . . . . . . . . 16 𝑥((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)
28 nfcv 2747 . . . . . . . . . . . . . . . 16 𝑥𝑧
2927, 28nffv 6092 . . . . . . . . . . . . . . 15 𝑥(((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧)
30 nffvmpt1 6093 . . . . . . . . . . . . . . . 16 𝑥((𝑥𝑍𝐴)‘𝑘)
3130, 28nffv 6092 . . . . . . . . . . . . . . 15 𝑥(((𝑥𝑍𝐴)‘𝑘)‘𝑧)
3229, 31nfeq 2758 . . . . . . . . . . . . . 14 𝑥(((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)
3326, 32nfral 2925 . . . . . . . . . . . . 13 𝑥𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)
34 fveq2 6085 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥) = ((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘))
3534fveq1d 6087 . . . . . . . . . . . . . . 15 (𝑥 = 𝑘 → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧))
36 fveq2 6085 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → ((𝑥𝑍𝐴)‘𝑥) = ((𝑥𝑍𝐴)‘𝑘))
3736fveq1d 6087 . . . . . . . . . . . . . . 15 (𝑥 = 𝑘 → (((𝑥𝑍𝐴)‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
3835, 37eqeq12d 2621 . . . . . . . . . . . . . 14 (𝑥 = 𝑘 → ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧) ↔ (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)))
3938ralbidv 2965 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → (∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧) ↔ ∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧)))
4025, 33, 39cbvral 3139 . . . . . . . . . . . 12 (∀𝑥𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑥)‘𝑧) = (((𝑥𝑍𝐴)‘𝑥)‘𝑧) ↔ ∀𝑘𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
4124, 40sylib 206 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝑍𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
4241r19.21bi 2912 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
43 oveq1 6531 . . . . . . . . . . . . 13 ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧)) = ((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧)))
4443fveq2d 6089 . . . . . . . . . . . 12 ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) = (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))))
4544breq1d 4584 . . . . . . . . . . 11 ((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → ((abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
4645ralimi 2932 . . . . . . . . . 10 (∀𝑧𝑇 (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧) → ∀𝑧𝑇 ((abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
47 ralbi 3046 . . . . . . . . . 10 (∀𝑧𝑇 ((abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟) → (∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
4842, 46, 473syl 18 . . . . . . . . 9 ((𝜑𝑘𝑍) → (∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 ↔ ∀𝑧𝑇 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
497, 48sylibrd 247 . . . . . . . 8 ((𝜑𝑘𝑍) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
503, 49sylan2 489 . . . . . . 7 ((𝜑 ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5150anassrs 677 . . . . . 6 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5251ralimdva 2941 . . . . 5 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5352reximdva 2996 . . . 4 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
5453ralimdv 2942 . . 3 (𝜑 → (∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
55 ulmf 23854 . . . . . 6 ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺 → ∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆))
561, 55syl 17 . . . . 5 (𝜑 → ∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆))
57 fdm 5947 . . . . . . . 8 ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆) → dom (𝑥𝑍𝐴) = (ℤ𝑚))
5819dmmptss 5531 . . . . . . . 8 dom (𝑥𝑍𝐴) ⊆ 𝑍
5957, 58syl6eqssr 3615 . . . . . . 7 ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆) → (ℤ𝑚) ⊆ 𝑍)
60 uzid 11531 . . . . . . . . 9 (𝑚 ∈ ℤ → 𝑚 ∈ (ℤ𝑚))
6160adantl 480 . . . . . . . 8 ((𝜑𝑚 ∈ ℤ) → 𝑚 ∈ (ℤ𝑚))
62 ssel 3558 . . . . . . . . 9 ((ℤ𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ𝑚) → 𝑚𝑍))
63 eluzel2 11521 . . . . . . . . . 10 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
6463, 2eleq2s 2702 . . . . . . . . 9 (𝑚𝑍𝑀 ∈ ℤ)
6562, 64syl6 34 . . . . . . . 8 ((ℤ𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ𝑚) → 𝑀 ∈ ℤ))
6661, 65syl5com 31 . . . . . . 7 ((𝜑𝑚 ∈ ℤ) → ((ℤ𝑚) ⊆ 𝑍𝑀 ∈ ℤ))
6759, 66syl5 33 . . . . . 6 ((𝜑𝑚 ∈ ℤ) → ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆) → 𝑀 ∈ ℤ))
6867rexlimdva 3009 . . . . 5 (𝜑 → (∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆) → 𝑀 ∈ ℤ))
6956, 68mpd 15 . . . 4 (𝜑𝑀 ∈ ℤ)
7011ralrimiva 2945 . . . . . 6 (𝜑 → ∀𝑥𝑍 𝐴𝑊)
7119fnmpt 5916 . . . . . 6 (∀𝑥𝑍 𝐴𝑊 → (𝑥𝑍𝐴) Fn 𝑍)
7270, 71syl 17 . . . . 5 (𝜑 → (𝑥𝑍𝐴) Fn 𝑍)
73 frn 5949 . . . . . . 7 ((𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆) → ran (𝑥𝑍𝐴) ⊆ (ℂ ↑𝑚 𝑆))
7473rexlimivw 3007 . . . . . 6 (∃𝑚 ∈ ℤ (𝑥𝑍𝐴):(ℤ𝑚)⟶(ℂ ↑𝑚 𝑆) → ran (𝑥𝑍𝐴) ⊆ (ℂ ↑𝑚 𝑆))
7556, 74syl 17 . . . . 5 (𝜑 → ran (𝑥𝑍𝐴) ⊆ (ℂ ↑𝑚 𝑆))
76 df-f 5791 . . . . 5 ((𝑥𝑍𝐴):𝑍⟶(ℂ ↑𝑚 𝑆) ↔ ((𝑥𝑍𝐴) Fn 𝑍 ∧ ran (𝑥𝑍𝐴) ⊆ (ℂ ↑𝑚 𝑆)))
7772, 75, 76sylanbrc 694 . . . 4 (𝜑 → (𝑥𝑍𝐴):𝑍⟶(ℂ ↑𝑚 𝑆))
78 eqidd 2607 . . . 4 ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (((𝑥𝑍𝐴)‘𝑘)‘𝑧) = (((𝑥𝑍𝐴)‘𝑘)‘𝑧))
79 eqidd 2607 . . . 4 ((𝜑𝑧𝑆) → (𝐺𝑧) = (𝐺𝑧))
80 ulmcl 23853 . . . . 5 ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺𝐺:𝑆⟶ℂ)
811, 80syl 17 . . . 4 (𝜑𝐺:𝑆⟶ℂ)
82 ulmscl 23851 . . . . 5 ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺𝑆 ∈ V)
831, 82syl 17 . . . 4 (𝜑𝑆 ∈ V)
842, 69, 77, 78, 79, 81, 83ulm2 23857 . . 3 (𝜑 → ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺 ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘((((𝑥𝑍𝐴)‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
8519fmpt 6271 . . . . . . . . . 10 (∀𝑥𝑍 𝐴 ∈ (ℂ ↑𝑚 𝑆) ↔ (𝑥𝑍𝐴):𝑍⟶(ℂ ↑𝑚 𝑆))
8677, 85sylibr 222 . . . . . . . . 9 (𝜑 → ∀𝑥𝑍 𝐴 ∈ (ℂ ↑𝑚 𝑆))
8786r19.21bi 2912 . . . . . . . 8 ((𝜑𝑥𝑍) → 𝐴 ∈ (ℂ ↑𝑚 𝑆))
88 elmapi 7739 . . . . . . . 8 (𝐴 ∈ (ℂ ↑𝑚 𝑆) → 𝐴:𝑆⟶ℂ)
8987, 88syl 17 . . . . . . 7 ((𝜑𝑥𝑍) → 𝐴:𝑆⟶ℂ)
904adantr 479 . . . . . . 7 ((𝜑𝑥𝑍) → 𝑇𝑆)
9189, 90fssresd 5966 . . . . . 6 ((𝜑𝑥𝑍) → (𝐴𝑇):𝑇⟶ℂ)
92 cnex 9870 . . . . . . 7 ℂ ∈ V
9383, 4ssexd 4725 . . . . . . . 8 (𝜑𝑇 ∈ V)
9493adantr 479 . . . . . . 7 ((𝜑𝑥𝑍) → 𝑇 ∈ V)
95 elmapg 7731 . . . . . . 7 ((ℂ ∈ V ∧ 𝑇 ∈ V) → ((𝐴𝑇) ∈ (ℂ ↑𝑚 𝑇) ↔ (𝐴𝑇):𝑇⟶ℂ))
9692, 94, 95sylancr 693 . . . . . 6 ((𝜑𝑥𝑍) → ((𝐴𝑇) ∈ (ℂ ↑𝑚 𝑇) ↔ (𝐴𝑇):𝑇⟶ℂ))
9791, 96mpbird 245 . . . . 5 ((𝜑𝑥𝑍) → (𝐴𝑇) ∈ (ℂ ↑𝑚 𝑇))
9897, 15fmptd 6274 . . . 4 (𝜑 → (𝑥𝑍 ↦ (𝐴𝑇)):𝑍⟶(ℂ ↑𝑚 𝑇))
99 eqidd 2607 . . . 4 ((𝜑 ∧ (𝑘𝑍𝑧𝑇)) → (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) = (((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧))
100 fvres 6099 . . . . 5 (𝑧𝑇 → ((𝐺𝑇)‘𝑧) = (𝐺𝑧))
101100adantl 480 . . . 4 ((𝜑𝑧𝑇) → ((𝐺𝑇)‘𝑧) = (𝐺𝑧))
10281, 4fssresd 5966 . . . 4 (𝜑 → (𝐺𝑇):𝑇⟶ℂ)
1032, 69, 98, 99, 101, 102, 93ulm2 23857 . . 3 (𝜑 → ((𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇) ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑇 (abs‘((((𝑥𝑍 ↦ (𝐴𝑇))‘𝑘)‘𝑧) − (𝐺𝑧))) < 𝑟))
10454, 84, 1033imtr4d 281 . 2 (𝜑 → ((𝑥𝑍𝐴)(⇝𝑢𝑆)𝐺 → (𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇)))
1051, 104mpd 15 1 (𝜑 → (𝑥𝑍 ↦ (𝐴𝑇))(⇝𝑢𝑇)(𝐺𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2892  wrex 2893  Vcvv 3169  wss 3536   class class class wbr 4574  cmpt 4634  dom cdm 5025  ran crn 5026  cres 5027   Fn wfn 5782  wf 5783  cfv 5787  (class class class)co 6524  𝑚 cmap 7718  cc 9787   < clt 9927  cmin 10114  cz 11207  cuz 11516  +crp 11661  abscabs 13765  𝑢culm 23848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-pre-lttri 9863  ax-pre-lttrn 9864
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-po 4946  df-so 4947  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-1st 7033  df-2nd 7034  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-neg 10117  df-z 11208  df-uz 11517  df-ulm 23849
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator