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 tgioo4 ⊢ ( 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 )