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 
|- ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( G o. F ) e. MblFn )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> G e. ( B -cn-> CC ) )
2 cncff 
 |-  ( G e. ( B -cn-> CC ) -> G : B --> CC )
3 1 2 syl 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> G : B --> CC )
4 simp2 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> F : A --> B )
5 fco 
 |-  ( ( G : B --> CC /\ F : A --> B ) -> ( G o. F ) : A --> CC )
6 3 4 5 syl2anc 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( G o. F ) : A --> CC )
7 4 fdmd 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> dom F = A )
8 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
9 8 3ad2ant1 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> dom F e. dom vol )
10 7 9 eqeltrrd 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> A e. dom vol )
11 mblss 
 |-  ( A e. dom vol -> A C_ RR )
12 10 11 syl 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> A C_ RR )
13 cnex 
 |-  CC e. _V
14 reex 
 |-  RR e. _V
15 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( ( G o. F ) : A --> CC /\ A C_ RR ) ) -> ( G o. F ) e. ( CC ^pm RR ) )
16 13 14 15 mpanl12 
 |-  ( ( ( G o. F ) : A --> CC /\ A C_ RR ) -> ( G o. F ) e. ( CC ^pm RR ) )
17 6 12 16 syl2anc 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( G o. F ) e. ( CC ^pm RR ) )
18 coeq1 
 |-  ( g = ( Re o. G ) -> ( g o. F ) = ( ( Re o. G ) o. F ) )
19 coass 
 |-  ( ( Re o. G ) o. F ) = ( Re o. ( G o. F ) )
20 18 19 eqtrdi 
 |-  ( g = ( Re o. G ) -> ( g o. F ) = ( Re o. ( G o. F ) ) )
21 20 cnveqd 
 |-  ( g = ( Re o. G ) -> `' ( g o. F ) = `' ( Re o. ( G o. F ) ) )
22 21 imaeq1d 
 |-  ( g = ( Re o. G ) -> ( `' ( g o. F ) " x ) = ( `' ( Re o. ( G o. F ) ) " x ) )
23 22 eleq1d 
 |-  ( g = ( Re o. G ) -> ( ( `' ( g o. F ) " x ) e. dom vol <-> ( `' ( Re o. ( G o. F ) ) " x ) e. dom vol ) )
24 cnvco 
 |-  `' ( g o. F ) = ( `' F o. `' g )
25 24 imaeq1i 
 |-  ( `' ( g o. F ) " x ) = ( ( `' F o. `' g ) " x )
26 imaco 
 |-  ( ( `' F o. `' g ) " x ) = ( `' F " ( `' g " x ) )
27 25 26 eqtri 
 |-  ( `' ( g o. F ) " x ) = ( `' F " ( `' g " x ) )
28 simplll 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> F e. MblFn )
29 simpllr 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> F : A --> B )
30 cncfrss 
 |-  ( g e. ( B -cn-> RR ) -> B C_ CC )
31 30 adantl 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> B C_ CC )
32 simpr 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> g e. ( B -cn-> RR ) )
33 ax-resscn 
 |-  RR C_ CC
34 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
35 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t B ) = ( ( TopOpen ` CCfld ) |`t B )
36 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
37 34 35 36 cncfcn 
 |-  ( ( B C_ CC /\ RR C_ CC ) -> ( B -cn-> RR ) = ( ( ( TopOpen ` CCfld ) |`t B ) Cn ( topGen ` ran (,) ) ) )
38 31 33 37 sylancl 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> ( B -cn-> RR ) = ( ( ( TopOpen ` CCfld ) |`t B ) Cn ( topGen ` ran (,) ) ) )
39 32 38 eleqtrd 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> g e. ( ( ( TopOpen ` CCfld ) |`t B ) Cn ( topGen ` ran (,) ) ) )
40 retopbas 
 |-  ran (,) e. TopBases
41 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
42 40 41 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
43 simplr 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> x e. ran (,) )
44 42 43 sselid 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> x e. ( topGen ` ran (,) ) )
45 cnima 
 |-  ( ( g e. ( ( ( TopOpen ` CCfld ) |`t B ) Cn ( topGen ` ran (,) ) ) /\ x e. ( topGen ` ran (,) ) ) -> ( `' g " x ) e. ( ( TopOpen ` CCfld ) |`t B ) )
46 39 44 45 syl2anc 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> ( `' g " x ) e. ( ( TopOpen ` CCfld ) |`t B ) )
47 34 35 mbfimaopn2 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ ( `' g " x ) e. ( ( TopOpen ` CCfld ) |`t B ) ) -> ( `' F " ( `' g " x ) ) e. dom vol )
48 28 29 31 46 47 syl31anc 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> ( `' F " ( `' g " x ) ) e. dom vol )
49 27 48 eqeltrid 
 |-  ( ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) /\ g e. ( B -cn-> RR ) ) -> ( `' ( g o. F ) " x ) e. dom vol )
50 49 ralrimiva 
 |-  ( ( ( F e. MblFn /\ F : A --> B ) /\ x e. ran (,) ) -> A. g e. ( B -cn-> RR ) ( `' ( g o. F ) " x ) e. dom vol )
51 50 3adantl3 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) /\ x e. ran (,) ) -> A. g e. ( B -cn-> RR ) ( `' ( g o. F ) " x ) e. dom vol )
52 recncf 
 |-  Re e. ( CC -cn-> RR )
53 52 a1i 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> Re e. ( CC -cn-> RR ) )
54 1 53 cncfco 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( Re o. G ) e. ( B -cn-> RR ) )
55 54 adantr 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) /\ x e. ran (,) ) -> ( Re o. G ) e. ( B -cn-> RR ) )
56 23 51 55 rspcdva 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) /\ x e. ran (,) ) -> ( `' ( Re o. ( G o. F ) ) " x ) e. dom vol )
57 coeq1 
 |-  ( g = ( Im o. G ) -> ( g o. F ) = ( ( Im o. G ) o. F ) )
58 coass 
 |-  ( ( Im o. G ) o. F ) = ( Im o. ( G o. F ) )
59 57 58 eqtrdi 
 |-  ( g = ( Im o. G ) -> ( g o. F ) = ( Im o. ( G o. F ) ) )
60 59 cnveqd 
 |-  ( g = ( Im o. G ) -> `' ( g o. F ) = `' ( Im o. ( G o. F ) ) )
61 60 imaeq1d 
 |-  ( g = ( Im o. G ) -> ( `' ( g o. F ) " x ) = ( `' ( Im o. ( G o. F ) ) " x ) )
62 61 eleq1d 
 |-  ( g = ( Im o. G ) -> ( ( `' ( g o. F ) " x ) e. dom vol <-> ( `' ( Im o. ( G o. F ) ) " x ) e. dom vol ) )
63 imcncf 
 |-  Im e. ( CC -cn-> RR )
64 63 a1i 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> Im e. ( CC -cn-> RR ) )
65 1 64 cncfco 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( Im o. G ) e. ( B -cn-> RR ) )
66 65 adantr 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) /\ x e. ran (,) ) -> ( Im o. G ) e. ( B -cn-> RR ) )
67 62 51 66 rspcdva 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) /\ x e. ran (,) ) -> ( `' ( Im o. ( G o. F ) ) " x ) e. dom vol )
68 56 67 jca 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) /\ x e. ran (,) ) -> ( ( `' ( Re o. ( G o. F ) ) " x ) e. dom vol /\ ( `' ( Im o. ( G o. F ) ) " x ) e. dom vol ) )
69 68 ralrimiva 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> A. x e. ran (,) ( ( `' ( Re o. ( G o. F ) ) " x ) e. dom vol /\ ( `' ( Im o. ( G o. F ) ) " x ) e. dom vol ) )
70 ismbf1 
 |-  ( ( G o. F ) e. MblFn <-> ( ( G o. F ) e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. ( G o. F ) ) " x ) e. dom vol /\ ( `' ( Im o. ( G o. F ) ) " x ) e. dom vol ) ) )
71 17 69 70 sylanbrc 
 |-  ( ( F e. MblFn /\ F : A --> B /\ G e. ( B -cn-> CC ) ) -> ( G o. F ) e. MblFn )