Metamath Proof Explorer

Theorem cxpcncf1

Description: The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn . (Contributed by Thierry Arnoux, 20-Dec-2021)

Ref Expression
Hypotheses cxpcncf1.a 
|- ( ph -> A e. CC )
cxpcncf1.d 
|- ( ph -> D C_ ( CC \ ( -oo (,] 0 ) ) )
Assertion cxpcncf1 
|- ( ph -> ( x e. D |-> ( x ^c A ) ) e. ( D -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cxpcncf1.a 
 |-  ( ph -> A e. CC )
2 cxpcncf1.d 
 |-  ( ph -> D C_ ( CC \ ( -oo (,] 0 ) ) )
3 resmpt 
 |-  ( D C_ ( CC \ ( -oo (,] 0 ) ) -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) |` D ) = ( x e. D |-> ( x ^c A ) ) )
4 2 3 syl 
 |-  ( ph -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) |` D ) = ( x e. D |-> ( x ^c A ) ) )
5 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
6 5 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
7 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
8 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( CC \ ( -oo (,] 0 ) ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) )
9 6 7 8 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) )
10 9 a1i 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) )
11 10 cnmptid 
 |-  ( ph -> ( x e. ( CC \ ( -oo (,] 0 ) ) |-> x ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) ) )
12 6 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
13 10 12 1 cnmptc 
 |-  ( ph -> ( x e. ( CC \ ( -oo (,] 0 ) ) |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( TopOpen ` CCfld ) ) )
14 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
15 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) )
16 14 5 15 cxpcn 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) , z e. CC |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
17 16 a1i 
 |-  ( ph -> ( y e. ( CC \ ( -oo (,] 0 ) ) , z e. CC |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
18 oveq12 
 |-  ( ( y = x /\ z = A ) -> ( y ^c z ) = ( x ^c A ) )
19 10 11 13 10 12 17 18 cnmpt12 
 |-  ( ph -> ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( TopOpen ` CCfld ) ) )
20 ssid 
 |-  CC C_ CC
21 6 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
22 5 15 21 cncfcn 
 |-  ( ( ( CC \ ( -oo (,] 0 ) ) C_ CC /\ CC C_ CC ) -> ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( TopOpen ` CCfld ) ) )
23 7 20 22 mp2an 
 |-  ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( TopOpen ` CCfld ) )
24 23 eqcomi 
 |-  ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( TopOpen ` CCfld ) ) = ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC )
25 24 a1i 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) Cn ( TopOpen ` CCfld ) ) = ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) )
26 19 25 eleqtrd 
 |-  ( ph -> ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) )
27 rescncf 
 |-  ( D C_ ( CC \ ( -oo (,] 0 ) ) -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) |` D ) e. ( D -cn-> CC ) ) )
28 27 imp 
 |-  ( ( D C_ ( CC \ ( -oo (,] 0 ) ) /\ ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) e. ( ( CC \ ( -oo (,] 0 ) ) -cn-> CC ) ) -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) |` D ) e. ( D -cn-> CC ) )
29 2 26 28 syl2anc 
 |-  ( ph -> ( ( x e. ( CC \ ( -oo (,] 0 ) ) |-> ( x ^c A ) ) |` D ) e. ( D -cn-> CC ) )
30 4 29 eqeltrrd 
 |-  ( ph -> ( x e. D |-> ( x ^c A ) ) e. ( D -cn-> CC ) )