Metamath Proof Explorer


Theorem mbfadd

Description: The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses mbfadd.1 φFMblFn
mbfadd.2 φGMblFn
Assertion mbfadd φF+fGMblFn

Proof

Step Hyp Ref Expression
1 mbfadd.1 φFMblFn
2 mbfadd.2 φGMblFn
3 mbff FMblFnF:domF
4 1 3 syl φF:domF
5 4 ffnd φFFndomF
6 mbff GMblFnG:domG
7 2 6 syl φG:domG
8 7 ffnd φGFndomG
9 mbfdm FMblFndomFdomvol
10 1 9 syl φdomFdomvol
11 mbfdm GMblFndomGdomvol
12 2 11 syl φdomGdomvol
13 eqid domFdomG=domFdomG
14 eqidd φxdomFFx=Fx
15 eqidd φxdomGGx=Gx
16 5 8 10 12 13 14 15 offval φF+fG=xdomFdomGFx+Gx
17 elinel1 xdomFdomGxdomF
18 ffvelcdm F:domFxdomFFx
19 4 17 18 syl2an φxdomFdomGFx
20 elinel2 xdomFdomGxdomG
21 ffvelcdm G:domGxdomGGx
22 7 20 21 syl2an φxdomFdomGGx
23 19 22 readdd φxdomFdomGFx+Gx=Fx+Gx
24 23 mpteq2dva φxdomFdomGFx+Gx=xdomFdomGFx+Gx
25 inmbl domFdomvoldomGdomvoldomFdomGdomvol
26 10 12 25 syl2anc φdomFdomGdomvol
27 19 recld φxdomFdomGFx
28 22 recld φxdomFdomGGx
29 eqidd φxdomFdomGFx=xdomFdomGFx
30 eqidd φxdomFdomGGx=xdomFdomGGx
31 26 27 28 29 30 offval2 φxdomFdomGFx+fxdomFdomGGx=xdomFdomGFx+Gx
32 24 31 eqtr4d φxdomFdomGFx+Gx=xdomFdomGFx+fxdomFdomGGx
33 inss1 domFdomGdomF
34 resmpt domFdomGdomFxdomFFxdomFdomG=xdomFdomGFx
35 33 34 ax-mp xdomFFxdomFdomG=xdomFdomGFx
36 4 feqmptd φF=xdomFFx
37 36 1 eqeltrrd φxdomFFxMblFn
38 mbfres xdomFFxMblFndomFdomGdomvolxdomFFxdomFdomGMblFn
39 37 26 38 syl2anc φxdomFFxdomFdomGMblFn
40 35 39 eqeltrrid φxdomFdomGFxMblFn
41 19 ismbfcn2 φxdomFdomGFxMblFnxdomFdomGFxMblFnxdomFdomGFxMblFn
42 40 41 mpbid φxdomFdomGFxMblFnxdomFdomGFxMblFn
43 42 simpld φxdomFdomGFxMblFn
44 inss2 domFdomGdomG
45 resmpt domFdomGdomGxdomGGxdomFdomG=xdomFdomGGx
46 44 45 ax-mp xdomGGxdomFdomG=xdomFdomGGx
47 7 feqmptd φG=xdomGGx
48 47 2 eqeltrrd φxdomGGxMblFn
49 mbfres xdomGGxMblFndomFdomGdomvolxdomGGxdomFdomGMblFn
50 48 26 49 syl2anc φxdomGGxdomFdomGMblFn
51 46 50 eqeltrrid φxdomFdomGGxMblFn
52 22 ismbfcn2 φxdomFdomGGxMblFnxdomFdomGGxMblFnxdomFdomGGxMblFn
53 51 52 mpbid φxdomFdomGGxMblFnxdomFdomGGxMblFn
54 53 simpld φxdomFdomGGxMblFn
55 27 fmpttd φxdomFdomGFx:domFdomG
56 28 fmpttd φxdomFdomGGx:domFdomG
57 43 54 55 56 mbfaddlem φxdomFdomGFx+fxdomFdomGGxMblFn
58 32 57 eqeltrd φxdomFdomGFx+GxMblFn
59 19 22 imaddd φxdomFdomGFx+Gx=Fx+Gx
60 59 mpteq2dva φxdomFdomGFx+Gx=xdomFdomGFx+Gx
61 19 imcld φxdomFdomGFx
62 22 imcld φxdomFdomGGx
63 eqidd φxdomFdomGFx=xdomFdomGFx
64 eqidd φxdomFdomGGx=xdomFdomGGx
65 26 61 62 63 64 offval2 φxdomFdomGFx+fxdomFdomGGx=xdomFdomGFx+Gx
66 60 65 eqtr4d φxdomFdomGFx+Gx=xdomFdomGFx+fxdomFdomGGx
67 42 simprd φxdomFdomGFxMblFn
68 53 simprd φxdomFdomGGxMblFn
69 61 fmpttd φxdomFdomGFx:domFdomG
70 62 fmpttd φxdomFdomGGx:domFdomG
71 67 68 69 70 mbfaddlem φxdomFdomGFx+fxdomFdomGGxMblFn
72 66 71 eqeltrd φxdomFdomGFx+GxMblFn
73 19 22 addcld φxdomFdomGFx+Gx
74 73 ismbfcn2 φxdomFdomGFx+GxMblFnxdomFdomGFx+GxMblFnxdomFdomGFx+GxMblFn
75 58 72 74 mpbir2and φxdomFdomGFx+GxMblFn
76 16 75 eqeltrd φF+fGMblFn