Metamath Proof Explorer

Theorem cxpcncf2

Description: The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion cxpcncf2 
|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> ( A ^c x ) ) e. ( CC -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
3 2 a1i 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
4 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
5 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( CC \ ( -oo (,] 0 ) ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) )
6 2 4 5 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) )
7 6 a1i 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) )
8 id 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> A e. ( CC \ ( -oo (,] 0 ) ) )
9 snidg 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> A e. { A } )
10 9 adantr 
 |-  ( ( A e. ( CC \ ( -oo (,] 0 ) ) /\ x e. CC ) -> A e. { A } )
11 10 fmpttd 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> A ) : CC --> { A } )
12 cnconst 
 |-  ( ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) e. ( TopOn ` ( CC \ ( -oo (,] 0 ) ) ) ) /\ ( A e. ( CC \ ( -oo (,] 0 ) ) /\ ( x e. CC |-> A ) : CC --> { A } ) ) -> ( x e. CC |-> A ) e. ( ( TopOpen ` CCfld ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) ) )
13 3 7 8 11 12 syl22anc 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> A ) e. ( ( TopOpen ` CCfld ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) ) )
14 3 cnmptid 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> x ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
15 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
16 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) )
17 15 1 16 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 ) )
18 17 a1i 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( y e. ( CC \ ( -oo (,] 0 ) ) , z e. CC |-> ( y ^c z ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( CC \ ( -oo (,] 0 ) ) ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
19 oveq12 
 |-  ( ( y = A /\ z = x ) -> ( y ^c z ) = ( A ^c x ) )
20 3 13 14 7 3 18 19 cnmpt12 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> ( A ^c x ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
21 ssid 
 |-  CC C_ CC
22 2 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
23 1 22 22 cncfcn 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
24 21 21 23 mp2an 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
25 24 eqcomi 
 |-  ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) = ( CC -cn-> CC )
26 25 a1i 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) = ( CC -cn-> CC ) )
27 20 26 eleqtrd 
 |-  ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> ( A ^c x ) ) e. ( CC -cn-> CC ) )