Metamath Proof Explorer


Theorem mbfmcst

Description: A constant function is measurable. Cf. mbfconst . (Contributed by Thierry Arnoux, 26-Jan-2017)

Ref Expression
Hypotheses mbfmcst.1 φ S ran sigAlgebra
mbfmcst.2 φ T ran sigAlgebra
mbfmcst.3 φ F = x S A
mbfmcst.4 φ A T
Assertion mbfmcst φ F S MblFn μ T

Proof

Step Hyp Ref Expression
1 mbfmcst.1 φ S ran sigAlgebra
2 mbfmcst.2 φ T ran sigAlgebra
3 mbfmcst.3 φ F = x S A
4 mbfmcst.4 φ A T
5 4 adantr φ x S A T
6 3 5 fmpt3d φ F : S T
7 unielsiga T ran sigAlgebra T T
8 2 7 syl φ T T
9 unielsiga S ran sigAlgebra S S
10 1 9 syl φ S S
11 8 10 elmapd φ F T S F : S T
12 6 11 mpbird φ F T S
13 fconstmpt S × A = x S A
14 13 cnveqi S × A -1 = x S A -1
15 cnvxp S × A -1 = A × S
16 14 15 eqtr3i x S A -1 = A × S
17 16 imaeq1i x S A -1 y = A × S y
18 df-ima A × S y = ran A × S y
19 df-rn ran A × S y = dom A × S y -1
20 17 18 19 3eqtri x S A -1 y = dom A × S y -1
21 df-res A × S y = A × S y × V
22 inxp A × S y × V = A y × S V
23 inv1 S V = S
24 23 xpeq2i A y × S V = A y × S
25 21 22 24 3eqtri A × S y = A y × S
26 25 cnveqi A × S y -1 = A y × S -1
27 26 dmeqi dom A × S y -1 = dom A y × S -1
28 cnvxp A y × S -1 = S × A y
29 28 dmeqi dom A y × S -1 = dom S × A y
30 20 27 29 3eqtri x S A -1 y = dom S × A y
31 xpeq2 A y = S × A y = S ×
32 xp0 S × =
33 31 32 syl6eq A y = S × A y =
34 33 dmeqd A y = dom S × A y = dom
35 dm0 dom =
36 34 35 syl6eq A y = dom S × A y =
37 36 adantl φ A y = dom S × A y =
38 0elsiga S ran sigAlgebra S
39 1 38 syl φ S
40 39 adantr φ A y = S
41 37 40 eqeltrd φ A y = dom S × A y S
42 30 41 eqeltrid φ A y = x S A -1 y S
43 dmxp A y dom S × A y = S
44 43 adantl φ A y dom S × A y = S
45 10 adantr φ A y S S
46 44 45 eqeltrd φ A y dom S × A y S
47 30 46 eqeltrid φ A y x S A -1 y S
48 42 47 pm2.61dane φ x S A -1 y S
49 48 ralrimivw φ y T x S A -1 y S
50 3 cnveqd φ F -1 = x S A -1
51 50 imaeq1d φ F -1 y = x S A -1 y
52 51 eleq1d φ F -1 y S x S A -1 y S
53 52 ralbidv φ y T F -1 y S y T x S A -1 y S
54 49 53 mpbird φ y T F -1 y S
55 1 2 ismbfm φ F S MblFn μ T F T S y T F -1 y S
56 12 54 55 mpbir2and φ F S MblFn μ T