Metamath Proof Explorer

Theorem cncombf

Description: The composition of a continuous function with a measurable function is measurable. (More generally, G can be a Borel-measurable function, but notably the condition that G be only measurable is too weak, the usual counterexample taking G to be the Cantor function and F the indicator function of the G -image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion cncombf ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ( 𝐺 ∘ 𝐹 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → 𝐺 ∈ ( 𝐵 –cn→ ℂ ) )
2 cncff ⊢ ( 𝐺 ∈ ( 𝐵 –cn→ ℂ ) → 𝐺 : 𝐵 ⟶ ℂ )
3 1 2 syl ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → 𝐺 : 𝐵 ⟶ ℂ )
4 simp2 ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
5 fco ⊢ ( ( 𝐺 : 𝐵 ⟶ ℂ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ ℂ )
6 3 4 5 syl2anc ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ ℂ )
7 4 fdmd ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → dom 𝐹 = 𝐴 )
8 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
9 8 3ad2ant1 ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → dom 𝐹 ∈ dom vol )
10 7 9 eqeltrrd ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → 𝐴 ∈ dom vol )
11 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
12 10 11 syl ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → 𝐴 ⊆ ℝ )
13 cnex ⊢ ℂ ∈ V
14 reex ⊢ ℝ ∈ V
15 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( ℂ ↑pm ℝ ) )
16 13 14 15 mpanl12 ⊢ ( ( ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐺 ∘ 𝐹 ) ∈ ( ℂ ↑pm ℝ ) )
17 6 12 16 syl2anc ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ( 𝐺 ∘ 𝐹 ) ∈ ( ℂ ↑pm ℝ ) )
18 coeq1 ⊢ ( 𝑔 = ( ℜ ∘ 𝐺 ) → ( 𝑔 ∘ 𝐹 ) = ( ( ℜ ∘ 𝐺 ) ∘ 𝐹 ) )
19 coass ⊢ ( ( ℜ ∘ 𝐺 ) ∘ 𝐹 ) = ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) )
20 18 19 eqtrdi ⊢ ( 𝑔 = ( ℜ ∘ 𝐺 ) → ( 𝑔 ∘ 𝐹 ) = ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) )
21 20 cnveqd ⊢ ( 𝑔 = ( ℜ ∘ 𝐺 ) → ◡ ( 𝑔 ∘ 𝐹 ) = ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) )
22 21 imaeq1d ⊢ ( 𝑔 = ( ℜ ∘ 𝐺 ) → ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) = ( ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) )
23 22 eleq1d ⊢ ( 𝑔 = ( ℜ ∘ 𝐺 ) → ( ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ↔ ( ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ) )
24 cnvco ⊢ ◡ ( 𝑔 ∘ 𝐹 ) = ( ◡ 𝐹 ∘ ◡ 𝑔 )
25 24 imaeq1i ⊢ ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) = ( ( ◡ 𝐹 ∘ ◡ 𝑔 ) “ 𝑥 )
26 imaco ⊢ ( ( ◡ 𝐹 ∘ ◡ 𝑔 ) “ 𝑥 ) = ( ◡ 𝐹 “ ( ◡ 𝑔 “ 𝑥 ) )
27 25 26 eqtri ⊢ ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) = ( ◡ 𝐹 “ ( ◡ 𝑔 “ 𝑥 ) )
28 simplll ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝐹 ∈ MblFn )
29 simpllr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
30 cncfrss ⊢ ( 𝑔 ∈ ( 𝐵 –cn→ ℝ ) → 𝐵 ⊆ ℂ )
31 30 adantl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝐵 ⊆ ℂ )
32 simpr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝑔 ∈ ( 𝐵 –cn→ ℝ ) )
33 ax-resscn ⊢ ℝ ⊆ ℂ
34 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
35 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 )
36 34 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
37 34 35 36 cncfcn ⊢ ( ( 𝐵 ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝐵 –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) Cn ( topGen ‘ ran (,) ) ) )
38 31 33 37 sylancl ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → ( 𝐵 –cn→ ℝ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) Cn ( topGen ‘ ran (,) ) ) )
39 32 38 eleqtrd ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝑔 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) Cn ( topGen ‘ ran (,) ) ) )
40 retopbas ⊢ ran (,) ∈ TopBases
41 bastg ⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
42 40 41 ax-mp ⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
43 simplr ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝑥 ∈ ran (,) )
44 42 43 sselid ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → 𝑥 ∈ ( topGen ‘ ran (,) ) )
45 cnima ⊢ ( ( 𝑔 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) Cn ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ ( topGen ‘ ran (,) ) ) → ( ◡ 𝑔 “ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) )
46 39 44 45 syl2anc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → ( ◡ 𝑔 “ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) )
47 34 35 mbfimaopn2 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ⊆ ℂ ) ∧ ( ◡ 𝑔 “ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐵 ) ) → ( ◡ 𝐹 “ ( ◡ 𝑔 “ 𝑥 ) ) ∈ dom vol )
48 28 29 31 46 47 syl31anc ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → ( ◡ 𝐹 “ ( ◡ 𝑔 “ 𝑥 ) ) ∈ dom vol )
49 27 48 eqeltrid ⊢ ( ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) ∧ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ) → ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
50 49 ralrimiva ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ran (,) ) → ∀ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
51 50 3adantl3 ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ∀ 𝑔 ∈ ( 𝐵 –cn→ ℝ ) ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
52 recncf ⊢ ℜ ∈ ( ℂ –cn→ ℝ )
53 52 a1i ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ℜ ∈ ( ℂ –cn→ ℝ ) )
54 1 53 cncfco ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ( ℜ ∘ 𝐺 ) ∈ ( 𝐵 –cn→ ℝ ) )
55 54 adantr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ℜ ∘ 𝐺 ) ∈ ( 𝐵 –cn→ ℝ ) )
56 23 51 55 rspcdva ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol )
57 coeq1 ⊢ ( 𝑔 = ( ℑ ∘ 𝐺 ) → ( 𝑔 ∘ 𝐹 ) = ( ( ℑ ∘ 𝐺 ) ∘ 𝐹 ) )
58 coass ⊢ ( ( ℑ ∘ 𝐺 ) ∘ 𝐹 ) = ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) )
59 57 58 eqtrdi ⊢ ( 𝑔 = ( ℑ ∘ 𝐺 ) → ( 𝑔 ∘ 𝐹 ) = ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) )
60 59 cnveqd ⊢ ( 𝑔 = ( ℑ ∘ 𝐺 ) → ◡ ( 𝑔 ∘ 𝐹 ) = ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) )
61 60 imaeq1d ⊢ ( 𝑔 = ( ℑ ∘ 𝐺 ) → ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) = ( ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) )
62 61 eleq1d ⊢ ( 𝑔 = ( ℑ ∘ 𝐺 ) → ( ( ◡ ( 𝑔 ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ↔ ( ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ) )
63 imcncf ⊢ ℑ ∈ ( ℂ –cn→ ℝ )
64 63 a1i ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ℑ ∈ ( ℂ –cn→ ℝ ) )
65 1 64 cncfco ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ( ℑ ∘ 𝐺 ) ∈ ( 𝐵 –cn→ ℝ ) )
66 65 adantr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ℑ ∘ 𝐺 ) ∈ ( 𝐵 –cn→ ℝ ) )
67 62 51 66 rspcdva ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol )
68 56 67 jca ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) ∧ 𝑥 ∈ ran (,) ) → ( ( ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ) )
69 68 ralrimiva ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ) )
70 ismbf1 ⊢ ( ( 𝐺 ∘ 𝐹 ) ∈ MblFn ↔ ( ( 𝐺 ∘ 𝐹 ) ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ ( 𝐺 ∘ 𝐹 ) ) “ 𝑥 ) ∈ dom vol ) ) )
71 17 69 70 sylanbrc ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 ∈ ( 𝐵 –cn→ ℂ ) ) → ( 𝐺 ∘ 𝐹 ) ∈ MblFn )