cncfres

Description: A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypotheses	cncfres.1	⊢ 𝐴 ⊆ ℂ
	cncfres.2	⊢ 𝐵 ⊆ ℂ
	cncfres.3	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝐶 )
	cncfres.4	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	cncfres.5	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
	cncfres.6	⊢ 𝐹 ∈ ( ℂ –cn→ ℂ )
	cncfres.7	⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) )
	cncfres.8	⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) )
Assertion	cncfres	⊢ 𝐺 ∈ ( 𝐽 Cn 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cncfres.1	⊢ 𝐴 ⊆ ℂ
2		cncfres.2	⊢ 𝐵 ⊆ ℂ
3		cncfres.3	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝐶 )
4		cncfres.4	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
5		cncfres.5	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵 )
6		cncfres.6	⊢ 𝐹 ∈ ( ℂ –cn→ ℂ )
7		cncfres.7	⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) )
8		cncfres.8	⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) )
9	4 5	fmpti	⊢ 𝐺 : 𝐴 ⟶ 𝐵
10		resmpt	⊢ ( 𝐴 ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
11	1 10	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
12	4 11	eqtr4i	⊢ 𝐺 = ( ( 𝑥 ∈ ℂ ↦ 𝐶 ) ↾ 𝐴 )
13	3 6	eqeltrri	⊢ ( 𝑥 ∈ ℂ ↦ 𝐶 ) ∈ ( ℂ –cn→ ℂ )
14		rescncf	⊢ ( 𝐴 ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ 𝐶 ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ 𝐶 ) ↾ 𝐴 ) ∈ ( 𝐴 –cn→ ℂ ) ) )
15	1 13 14	mp2	⊢ ( ( 𝑥 ∈ ℂ ↦ 𝐶 ) ↾ 𝐴 ) ∈ ( 𝐴 –cn→ ℂ )
16	12 15	eqeltri	⊢ 𝐺 ∈ ( 𝐴 –cn→ ℂ )
17		cncffvrn	⊢ ( ( 𝐵 ⊆ ℂ ∧ 𝐺 ∈ ( 𝐴 –cn→ ℂ ) ) → ( 𝐺 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ 𝐺 : 𝐴 ⟶ 𝐵 ) )
18	2 16 17	mp2an	⊢ ( 𝐺 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ 𝐺 : 𝐴 ⟶ 𝐵 )
19	9 18	mpbir	⊢ 𝐺 ∈ ( 𝐴 –cn→ 𝐵 )
20		eqid	⊢ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) )
21		eqid	⊢ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) )
22	20 21 7 8	cncfmet	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( 𝐽 Cn 𝐾 ) )
23	1 2 22	mp2an	⊢ ( 𝐴 –cn→ 𝐵 ) = ( 𝐽 Cn 𝐾 )
24	19 23	eleqtri	⊢ 𝐺 ∈ ( 𝐽 Cn 𝐾 )

Metamath Proof Explorer

Theorem cncfres

Proof