Step |
Hyp |
Ref |
Expression |
1 |
|
mulcncf.1 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) ) |
2 |
|
mulcncf.2 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) ) |
3 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
4 |
3
|
cnfldtopon |
⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) |
5 |
|
cncfrss |
⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → 𝑋 ⊆ ℂ ) |
6 |
1 5
|
syl |
⊢ ( 𝜑 → 𝑋 ⊆ ℂ ) |
7 |
|
resttopon |
⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) ) |
8 |
4 6 7
|
sylancr |
⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) ) |
9 |
|
ssid |
⊢ ℂ ⊆ ℂ |
10 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) |
11 |
4
|
toponrestid |
⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) |
12 |
3 10 11
|
cncfcn |
⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) ) |
13 |
6 9 12
|
sylancl |
⊢ ( 𝜑 → ( 𝑋 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) ) |
14 |
1 13
|
eleqtrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) ) |
15 |
2 13
|
eleqtrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) ) |
16 |
4
|
a1i |
⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) |
17 |
3
|
mpomulcn |
⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
18 |
17
|
a1i |
⊢ ( 𝜑 → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ) |
19 |
|
oveq12 |
⊢ ( ( 𝑢 = 𝐴 ∧ 𝑣 = 𝐵 ) → ( 𝑢 · 𝑣 ) = ( 𝐴 · 𝐵 ) ) |
20 |
8 14 15 16 16 18 19
|
cnmpt12 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) Cn ( TopOpen ‘ ℂfld ) ) ) |
21 |
20 13
|
eleqtrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) ) |