Metamath Proof Explorer


Theorem mbfconst

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

Ref Expression
Assertion mbfconst A dom vol B A × B MblFn

Proof

Step Hyp Ref Expression
1 simplr A dom vol B x A B
2 fconstmpt A × B = x A B
3 1 2 fmptd A dom vol B A × B : A
4 mblss A dom vol A
5 4 adantr A dom vol B A
6 cnex V
7 reex V
8 elpm2r V V A × B : A A A × B 𝑝𝑚
9 6 7 8 mpanl12 A × B : A A A × B 𝑝𝑚
10 3 5 9 syl2anc A dom vol B A × B 𝑝𝑚
11 2 a1i A dom vol B A × B = x A B
12 ref :
13 12 a1i A dom vol B :
14 13 feqmptd A dom vol B = y y
15 fveq2 y = B y = B
16 1 11 14 15 fmptco A dom vol B A × B = x A B
17 fconstmpt A × B = x A B
18 16 17 syl6eqr A dom vol B A × B = A × B
19 18 cnveqd A dom vol B A × B -1 = A × B -1
20 19 imaeq1d A dom vol B A × B -1 y = A × B -1 y
21 recl B B
22 mbfconstlem A dom vol B A × B -1 y dom vol
23 21 22 sylan2 A dom vol B A × B -1 y dom vol
24 20 23 eqeltrd A dom vol B A × B -1 y dom vol
25 imf :
26 25 a1i A dom vol B :
27 26 feqmptd A dom vol B = y y
28 fveq2 y = B y = B
29 1 11 27 28 fmptco A dom vol B A × B = x A B
30 fconstmpt A × B = x A B
31 29 30 syl6eqr A dom vol B A × B = A × B
32 31 cnveqd A dom vol B A × B -1 = A × B -1
33 32 imaeq1d A dom vol B A × B -1 y = A × B -1 y
34 imcl B B
35 mbfconstlem A dom vol B A × B -1 y dom vol
36 34 35 sylan2 A dom vol B A × B -1 y dom vol
37 33 36 eqeltrd A dom vol B A × B -1 y dom vol
38 24 37 jca A dom vol B A × B -1 y dom vol A × B -1 y dom vol
39 38 ralrimivw A dom vol B y ran . A × B -1 y dom vol A × B -1 y dom vol
40 ismbf1 A × B MblFn A × B 𝑝𝑚 y ran . A × B -1 y dom vol A × B -1 y dom vol
41 10 39 40 sylanbrc A dom vol B A × B MblFn