Metamath Proof Explorer


Theorem cnmbf

Description: A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion cnmbf ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴cn→ ℂ ) ) → 𝐹 ∈ MblFn )

Proof

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 )