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	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )