Metamath Proof Explorer

Theorem mbfconst

Description: A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfconst 
|- ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) e. MblFn )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. dom vol /\ B e. CC ) /\ x e. A ) -> B e. CC )
2 fconstmpt 
 |-  ( A X. { B } ) = ( x e. A |-> B )
3 1 2 fmptd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) : A --> CC )
4 mblss 
 |-  ( A e. dom vol -> A C_ RR )
5 4 adantr 
 |-  ( ( A e. dom vol /\ B e. CC ) -> A C_ RR )
6 cnex 
 |-  CC e. _V
7 reex 
 |-  RR e. _V
8 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( ( A X. { B } ) : A --> CC /\ A C_ RR ) ) -> ( A X. { B } ) e. ( CC ^pm RR ) )
9 6 7 8 mpanl12 
 |-  ( ( ( A X. { B } ) : A --> CC /\ A C_ RR ) -> ( A X. { B } ) e. ( CC ^pm RR ) )
10 3 5 9 syl2anc 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) e. ( CC ^pm RR ) )
11 2 a1i 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) = ( x e. A |-> B ) )
12 ref 
 |-  Re : CC --> RR
13 12 a1i 
 |-  ( ( A e. dom vol /\ B e. CC ) -> Re : CC --> RR )
14 13 feqmptd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> Re = ( y e. CC |-> ( Re ` y ) ) )
15 fveq2 
 |-  ( y = B -> ( Re ` y ) = ( Re ` B ) )
16 1 11 14 15 fmptco 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( Re o. ( A X. { B } ) ) = ( x e. A |-> ( Re ` B ) ) )
17 fconstmpt 
 |-  ( A X. { ( Re ` B ) } ) = ( x e. A |-> ( Re ` B ) )
18 16 17 eqtr4di 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( Re o. ( A X. { B } ) ) = ( A X. { ( Re ` B ) } ) )
19 18 cnveqd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> `' ( Re o. ( A X. { B } ) ) = `' ( A X. { ( Re ` B ) } ) )
20 19 imaeq1d 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( `' ( Re o. ( A X. { B } ) ) " y ) = ( `' ( A X. { ( Re ` B ) } ) " y ) )
21 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
22 mbfconstlem 
 |-  ( ( A e. dom vol /\ ( Re ` B ) e. RR ) -> ( `' ( A X. { ( Re ` B ) } ) " y ) e. dom vol )
23 21 22 sylan2 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( `' ( A X. { ( Re ` B ) } ) " y ) e. dom vol )
24 20 23 eqeltrd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( `' ( Re o. ( A X. { B } ) ) " y ) e. dom vol )
25 imf 
 |-  Im : CC --> RR
26 25 a1i 
 |-  ( ( A e. dom vol /\ B e. CC ) -> Im : CC --> RR )
27 26 feqmptd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> Im = ( y e. CC |-> ( Im ` y ) ) )
28 fveq2 
 |-  ( y = B -> ( Im ` y ) = ( Im ` B ) )
29 1 11 27 28 fmptco 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( Im o. ( A X. { B } ) ) = ( x e. A |-> ( Im ` B ) ) )
30 fconstmpt 
 |-  ( A X. { ( Im ` B ) } ) = ( x e. A |-> ( Im ` B ) )
31 29 30 eqtr4di 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( Im o. ( A X. { B } ) ) = ( A X. { ( Im ` B ) } ) )
32 31 cnveqd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> `' ( Im o. ( A X. { B } ) ) = `' ( A X. { ( Im ` B ) } ) )
33 32 imaeq1d 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( `' ( Im o. ( A X. { B } ) ) " y ) = ( `' ( A X. { ( Im ` B ) } ) " y ) )
34 imcl 
 |-  ( B e. CC -> ( Im ` B ) e. RR )
35 mbfconstlem 
 |-  ( ( A e. dom vol /\ ( Im ` B ) e. RR ) -> ( `' ( A X. { ( Im ` B ) } ) " y ) e. dom vol )
36 34 35 sylan2 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( `' ( A X. { ( Im ` B ) } ) " y ) e. dom vol )
37 33 36 eqeltrd 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( `' ( Im o. ( A X. { B } ) ) " y ) e. dom vol )
38 24 37 jca 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( ( `' ( Re o. ( A X. { B } ) ) " y ) e. dom vol /\ ( `' ( Im o. ( A X. { B } ) ) " y ) e. dom vol ) )
39 38 ralrimivw 
 |-  ( ( A e. dom vol /\ B e. CC ) -> A. y e. ran (,) ( ( `' ( Re o. ( A X. { B } ) ) " y ) e. dom vol /\ ( `' ( Im o. ( A X. { B } ) ) " y ) e. dom vol ) )
40 ismbf1 
 |-  ( ( A X. { B } ) e. MblFn <-> ( ( A X. { B } ) e. ( CC ^pm RR ) /\ A. y e. ran (,) ( ( `' ( Re o. ( A X. { B } ) ) " y ) e. dom vol /\ ( `' ( Im o. ( A X. { B } ) ) " y ) e. dom vol ) ) )
41 10 39 40 sylanbrc 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) e. MblFn )