Metamath Proof Explorer

Theorem cxpcnOLD

Description: Obsolete version of cxpcn as of 17-Apr-2025. (Contributed by Mario Carneiro, 1-May-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cxpcnOLD.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
cxpcnOLD.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cxpcnOLD.k ⊢ 𝐾 = ( 𝐽 ↾t 𝐷 )
Assertion cxpcnOLD ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 cxpcnOLD.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 cxpcnOLD.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
3 cxpcnOLD.k ⊢ 𝐾 = ( 𝐽 ↾t 𝐷 )
4 1 ellogdm ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
5 4 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
6 5 adantr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → 𝑥 ∈ ℂ )
7 1 logdmn0 ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
8 7 adantr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → 𝑥 ≠ 0 )
9 simpr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
10 6 8 9 cxpefd ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ↑𝑐 𝑦 ) = ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) )
11 10 mpoeq3ia ⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) )
12 2 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
13 12 a1i ⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℂ ) )
14 5 ssriv ⊢ 𝐷 ⊆ ℂ
15 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
16 13 14 15 sylancl ⊢ ( ⊤ → ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
17 3 16 eqeltrid ⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ 𝐷 ) )
18 17 13 cnmpt2nd ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ 𝑦 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
19 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
20 19 adantr ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
21 20 mpoeq3ia ⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( log ‘ 𝑥 ) )
22 17 13 cnmpt1st ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ 𝑥 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐾 ) )
23 1 logcn ⊢ ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )
24 ssid ⊢ ℂ ⊆ ℂ
25 12 toponrestid ⊢ 𝐽 = ( 𝐽 ↾t ℂ )
26 2 3 25 cncfcn ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐷 –cn→ ℂ ) = ( 𝐾 Cn 𝐽 ) )
27 14 24 26 mp2an ⊢ ( 𝐷 –cn→ ℂ ) = ( 𝐾 Cn 𝐽 )
28 23 27 eleqtri ⊢ ( log ↾ 𝐷 ) ∈ ( 𝐾 Cn 𝐽 )
29 28 a1i ⊢ ( ⊤ → ( log ↾ 𝐷 ) ∈ ( 𝐾 Cn 𝐽 ) )
30 17 13 22 29 cnmpt21f ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
31 21 30 eqeltrrid ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( log ‘ 𝑥 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
32 2 mulcn ⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
33 32 a1i ⊢ ( ⊤ → · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
34 17 13 18 31 33 cnmpt22f ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
35 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
36 2 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 )
37 35 36 eleqtri ⊢ exp ∈ ( 𝐽 Cn 𝐽 )
38 37 a1i ⊢ ( ⊤ → exp ∈ ( 𝐽 Cn 𝐽 ) )
39 17 13 34 38 cnmpt21f ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
40 39 mptru ⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )
41 11 40 eqeltri ⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )