cncfcn

Description: Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Hypotheses	cncfcn.2	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	cncfcn.3	⊢ 𝐾 = ( 𝐽 ↾_t 𝐴 )
	cncfcn.4	⊢ 𝐿 = ( 𝐽 ↾_t 𝐵 )
Assertion	cncfcn	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( 𝐾 Cn 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfcn.2	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2		cncfcn.3	⊢ 𝐾 = ( 𝐽 ↾_t 𝐴 )
3		cncfcn.4	⊢ 𝐿 = ( 𝐽 ↾_t 𝐵 )
4		eqid	⊢ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) )
5		eqid	⊢ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) )
6		eqid	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) )
7		eqid	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) )
8	4 5 6 7	cncfmet	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) Cn ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) ) )
9		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
10		simpl	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐴 ⊆ ℂ )
11	1	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
12	4 11 6	metrest	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( 𝐽 ↾_t 𝐴 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
13	9 10 12	sylancr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐽 ↾_t 𝐴 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
14	2 13	eqtrid	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) )
15		simpr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐵 ⊆ ℂ )
16	5 11 7	metrest	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐵 ⊆ ℂ ) → ( 𝐽 ↾_t 𝐵 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) )
17	9 15 16	sylancr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐽 ↾_t 𝐵 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) )
18	3 17	eqtrid	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐿 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) )
19	14 18	oveq12d	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐾 Cn 𝐿 ) = ( ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐴 × 𝐴 ) ) ) Cn ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝐵 × 𝐵 ) ) ) ) )
20	8 19	eqtr4d	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = ( 𝐾 Cn 𝐿 ) )

Metamath Proof Explorer

Theorem cncfcn

Proof