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∈ℂ∖−∞0→x∈ℂ⟼Ax:ℂ⟶cnℂ

Proof

Step Hyp Ref Expression
1 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
2 1 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
3 2 a1i ⊢A∈ℂ∖−∞0→TopOpen⁡ℂfld∈TopOn⁡ℂ
4 difss ⊢ℂ∖−∞0⊆ℂ
5 resttopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ∧ℂ∖−∞0⊆ℂ→TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0
6 2 4 5 mp2an ⊢TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0
7 6 a1i ⊢A∈ℂ∖−∞0→TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0
8 id ⊢A∈ℂ∖−∞0→A∈ℂ∖−∞0
9 snidg ⊢A∈ℂ∖−∞0→A∈A
10 9 adantr ⊢A∈ℂ∖−∞0∧x∈ℂ→A∈A
11 10 fmpttd ⊢A∈ℂ∖−∞0→x∈ℂ⟼A:ℂ⟶A
12 cnconst ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ∧TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0∧A∈ℂ∖−∞0∧x∈ℂ⟼A:ℂ⟶A→x∈ℂ⟼A∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld↾𝑡ℂ∖−∞0
13 3 7 8 11 12 syl22anc ⊢A∈ℂ∖−∞0→x∈ℂ⟼A∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld↾𝑡ℂ∖−∞0
14 3 cnmptid ⊢A∈ℂ∖−∞0→x∈ℂ⟼x∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
15 eqid ⊢ℂ∖−∞0=ℂ∖−∞0
16 eqid ⊢TopOpen⁡ℂfld↾𝑡ℂ∖−∞0=TopOpen⁡ℂfld↾𝑡ℂ∖−∞0
17 15 1 16 cxpcn ⊢y∈ℂ∖−∞0,z∈ℂ⟼yz∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
18 17 a1i ⊢A∈ℂ∖−∞0→y∈ℂ∖−∞0,z∈ℂ⟼yz∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
19 oveq12 ⊢y=A∧z=x→yz=Ax
20 3 13 14 7 3 18 19 cnmpt12 ⊢A∈ℂ∖−∞0→x∈ℂ⟼Ax∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
21 ssid ⊢ℂ⊆ℂ
22 2 toponrestid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld↾𝑡ℂ
23 1 22 22 cncfcn ⊢ℂ⊆ℂ∧ℂ⊆ℂ→ℂ⟶cnℂ=TopOpen⁡ℂfldCnTopOpen⁡ℂfld
24 21 21 23 mp2an ⊢ℂ⟶cnℂ=TopOpen⁡ℂfldCnTopOpen⁡ℂfld
25 24 eqcomi ⊢TopOpen⁡ℂfldCnTopOpen⁡ℂfld=ℂ⟶cnℂ
26 25 a1i ⊢A∈ℂ∖−∞0→TopOpen⁡ℂfldCnTopOpen⁡ℂfld=ℂ⟶cnℂ
27 20 26 eleqtrd ⊢A∈ℂ∖−∞0→x∈ℂ⟼Ax:ℂ⟶cnℂ