Metamath Proof Explorer

Theorem 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 𝐿 ) )