# Metamath Proof Explorer

## Theorem mbfconst

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

Ref Expression
Assertion mbfconst ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {A}×\left\{{B}\right\}\in MblFn$

### Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\wedge {x}\in {A}\right)\to {B}\in ℂ$
2 fconstmpt ${⊢}{A}×\left\{{B}\right\}=\left({x}\in {A}⟼{B}\right)$
3 1 2 fmptd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \left({A}×\left\{{B}\right\}\right):{A}⟶ℂ$
4 mblss ${⊢}{A}\in \mathrm{dom}vol\to {A}\subseteq ℝ$
5 4 adantr ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {A}\subseteq ℝ$
6 cnex ${⊢}ℂ\in \mathrm{V}$
7 reex ${⊢}ℝ\in \mathrm{V}$
8 elpm2r ${⊢}\left(\left(ℂ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\wedge \left(\left({A}×\left\{{B}\right\}\right):{A}⟶ℂ\wedge {A}\subseteq ℝ\right)\right)\to {A}×\left\{{B}\right\}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
9 6 7 8 mpanl12 ${⊢}\left(\left({A}×\left\{{B}\right\}\right):{A}⟶ℂ\wedge {A}\subseteq ℝ\right)\to {A}×\left\{{B}\right\}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
10 3 5 9 syl2anc ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {A}×\left\{{B}\right\}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)$
11 2 a1i ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {A}×\left\{{B}\right\}=\left({x}\in {A}⟼{B}\right)$
12 ref ${⊢}\Re :ℂ⟶ℝ$
13 12 a1i ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Re :ℂ⟶ℝ$
14 13 feqmptd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Re =\left({y}\in ℂ⟼\Re \left({y}\right)\right)$
15 fveq2 ${⊢}{y}={B}\to \Re \left({y}\right)=\Re \left({B}\right)$
16 1 11 14 15 fmptco ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Re \circ \left({A}×\left\{{B}\right\}\right)=\left({x}\in {A}⟼\Re \left({B}\right)\right)$
17 fconstmpt ${⊢}{A}×\left\{\Re \left({B}\right)\right\}=\left({x}\in {A}⟼\Re \left({B}\right)\right)$
18 16 17 syl6eqr ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Re \circ \left({A}×\left\{{B}\right\}\right)={A}×\left\{\Re \left({B}\right)\right\}$
19 18 cnveqd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left(\Re \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}={\left({A}×\left\{\Re \left({B}\right)\right\}\right)}^{-1}$
20 19 imaeq1d ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left(\Re \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]={\left({A}×\left\{\Re \left({B}\right)\right\}\right)}^{-1}\left[{y}\right]$
21 recl ${⊢}{B}\in ℂ\to \Re \left({B}\right)\in ℝ$
22 mbfconstlem ${⊢}\left({A}\in \mathrm{dom}vol\wedge \Re \left({B}\right)\in ℝ\right)\to {\left({A}×\left\{\Re \left({B}\right)\right\}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
23 21 22 sylan2 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left({A}×\left\{\Re \left({B}\right)\right\}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
24 20 23 eqeltrd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left(\Re \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
25 imf ${⊢}\Im :ℂ⟶ℝ$
26 25 a1i ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Im :ℂ⟶ℝ$
27 26 feqmptd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Im =\left({y}\in ℂ⟼\Im \left({y}\right)\right)$
28 fveq2 ${⊢}{y}={B}\to \Im \left({y}\right)=\Im \left({B}\right)$
29 1 11 27 28 fmptco ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Im \circ \left({A}×\left\{{B}\right\}\right)=\left({x}\in {A}⟼\Im \left({B}\right)\right)$
30 fconstmpt ${⊢}{A}×\left\{\Im \left({B}\right)\right\}=\left({x}\in {A}⟼\Im \left({B}\right)\right)$
31 29 30 syl6eqr ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \Im \circ \left({A}×\left\{{B}\right\}\right)={A}×\left\{\Im \left({B}\right)\right\}$
32 31 cnveqd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left(\Im \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}={\left({A}×\left\{\Im \left({B}\right)\right\}\right)}^{-1}$
33 32 imaeq1d ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left(\Im \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]={\left({A}×\left\{\Im \left({B}\right)\right\}\right)}^{-1}\left[{y}\right]$
34 imcl ${⊢}{B}\in ℂ\to \Im \left({B}\right)\in ℝ$
35 mbfconstlem ${⊢}\left({A}\in \mathrm{dom}vol\wedge \Im \left({B}\right)\in ℝ\right)\to {\left({A}×\left\{\Im \left({B}\right)\right\}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
36 34 35 sylan2 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left({A}×\left\{\Im \left({B}\right)\right\}\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
37 33 36 eqeltrd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {\left(\Im \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol$
38 24 37 jca ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \left({\left(\Re \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol\right)$
39 38 ralrimivw ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to \forall {y}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol\right)$
40 ismbf1 ${⊢}{A}×\left\{{B}\right\}\in MblFn↔\left({A}×\left\{{B}\right\}\in \left(ℂ{↑}_{𝑝𝑚}ℝ\right)\wedge \forall {y}\in \mathrm{ran}\left(.\right)\phantom{\rule{.4em}{0ex}}\left({\left(\Re \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol\wedge {\left(\Im \circ \left({A}×\left\{{B}\right\}\right)\right)}^{-1}\left[{y}\right]\in \mathrm{dom}vol\right)\right)$
41 10 39 40 sylanbrc ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in ℂ\right)\to {A}×\left\{{B}\right\}\in MblFn$