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

Metamath Proof Explorer

Theorem rlimcn1

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014)

Ref Expression
Hypotheses rlimcn1.1 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑋 )
rlimcn1.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
rlimcn1.3 ⊢ ( 𝜑 → 𝐺 ⇝𝑟 𝐶 )
rlimcn1.4 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
rlimcn1.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
Assertion rlimcn1 ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rlimcn1.1 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑋 )
2 rlimcn1.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
3 rlimcn1.3 ⊢ ( 𝜑 → 𝐺 ⇝𝑟 𝐶 )
4 rlimcn1.4 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
5 rlimcn1.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
6 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑋 )
7 1 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
8 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑣 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑣 ) ) )
9 fveq2 ⊢ ( 𝑣 = ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) )
10 6 7 8 9 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) )
11 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ V )
12 11 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) ∈ V )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
14 7 3 eqbrtrrd ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ⇝𝑟 𝐶 )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) ⇝𝑟 𝐶 )
16 12 13 15 rlimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 ) )
17 fvoveq1 ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑤 ) → ( abs ‘ ( 𝑧 − 𝐶 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) )
18 17 breq1d ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑤 ) → ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 ) )
19 18 imbrov2fvoveq ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑤 ) → ( ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ↔ ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
20 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
21 6 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑋 )
22 19 20 21 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
23 22 imim2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 ) → ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
24 23 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 ) → ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
25 24 reximdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
26 25 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − 𝐶 ) ) < 𝑦 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) ) )
27 16 26 mpid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
28 27 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
29 5 28 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
31 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ℂ )
32 6 31 syldan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ℂ )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ℂ )
34 1 fdmd ⊢ ( 𝜑 → dom 𝐺 = 𝐴 )
35 rlimss ⊢ ( 𝐺 ⇝𝑟 𝐶 → dom 𝐺 ⊆ ℝ )
36 3 35 syl ⊢ ( 𝜑 → dom 𝐺 ⊆ ℝ )
37 34 36 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
38 4 2 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
39 33 37 38 rlim2 ⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑤 ∈ 𝐴 ( 𝑐 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) ) )
40 30 39 mpbird ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑤 ) ) ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )
41 10 40 eqbrtrd ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )