Step |
Hyp |
Ref |
Expression |
1 |
|
cncff |
⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ ) |
2 |
|
mblss |
⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ ) |
3 |
|
cnex |
⊢ ℂ ∈ V |
4 |
|
reex |
⊢ ℝ ∈ V |
5 |
|
elpm2r |
⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
6 |
3 4 5
|
mpanl12 |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
7 |
1 2 6
|
syl2anr |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
8 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → 𝐴 ∈ dom vol ) |
9 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) |
10 |
|
recncf |
⊢ ℜ ∈ ( ℂ –cn→ ℝ ) |
11 |
10
|
a1i |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ℜ ∈ ( ℂ –cn→ ℝ ) ) |
12 |
9 11
|
cncfco |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ℜ ∘ 𝐹 ) ∈ ( 𝐴 –cn→ ℝ ) ) |
13 |
2
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → 𝐴 ⊆ ℝ ) |
14 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
15 |
13 14
|
sstrdi |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → 𝐴 ⊆ ℂ ) |
16 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
17 |
|
eqid |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) |
18 |
16
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
19 |
16 17 18
|
cncfcn |
⊢ ( ( 𝐴 ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝐴 –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ) |
20 |
15 14 19
|
sylancl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( 𝐴 –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ) |
21 |
|
eqid |
⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) ) |
22 |
16 21
|
rerest |
⊢ ( 𝐴 ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) |
23 |
13 22
|
syl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) |
24 |
23
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ) |
25 |
20 24
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( 𝐴 –cn→ ℝ ) = ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ) |
26 |
12 25
|
eleqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ℜ ∘ 𝐹 ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ) |
27 |
|
retopbas |
⊢ ran (,) ∈ TopBases |
28 |
|
bastg |
⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) ) |
29 |
27 28
|
ax-mp |
⊢ ran (,) ⊆ ( topGen ‘ ran (,) ) |
30 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → 𝑥 ∈ ran (,) ) |
31 |
29 30
|
sselid |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → 𝑥 ∈ ( topGen ‘ ran (,) ) ) |
32 |
|
cnima |
⊢ ( ( ( ℜ ∘ 𝐹 ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ ( topGen ‘ ran (,) ) ) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) |
33 |
26 31 32
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) |
34 |
|
eqid |
⊢ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) |
35 |
34
|
subopnmbl |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) |
36 |
8 33 35
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) |
37 |
|
imcncf |
⊢ ℑ ∈ ( ℂ –cn→ ℝ ) |
38 |
37
|
a1i |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ℑ ∈ ( ℂ –cn→ ℝ ) ) |
39 |
9 38
|
cncfco |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ℑ ∘ 𝐹 ) ∈ ( 𝐴 –cn→ ℝ ) ) |
40 |
39 25
|
eleqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ℑ ∘ 𝐹 ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ) |
41 |
|
cnima |
⊢ ( ( ( ℑ ∘ 𝐹 ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) Cn ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ ( topGen ‘ ran (,) ) ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) |
42 |
40 31 41
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) |
43 |
34
|
subopnmbl |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) |
44 |
8 42 43
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) |
45 |
36 44
|
jca |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) |
46 |
45
|
ralrimiva |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) → ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) |
47 |
|
ismbf1 |
⊢ ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) ) |
48 |
7 46 47
|
sylanbrc |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) → 𝐹 ∈ MblFn ) |