mbfadd

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

	Ref	Expression
Hypotheses	mbfadd.1	$⊢ φ \to F \in MblFn$
	mbfadd.2	$⊢ φ \to G \in MblFn$
Assertion	mbfadd	$⊢ φ \to F +_{f} G \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfadd.1	$⊢ φ \to F \in MblFn$
2		mbfadd.2	$⊢ φ \to G \in MblFn$
3		mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$
4	1 3	syl	$⊢ φ \to F : dom F ⟶ ℂ$
5	4	ffnd	$⊢ φ \to F Fn dom F$
6		mbff	$⊢ G \in MblFn \to G : dom G ⟶ ℂ$
7	2 6	syl	$⊢ φ \to G : dom G ⟶ ℂ$
8	7	ffnd	$⊢ φ \to G Fn dom G$
9		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
10	1 9	syl	$⊢ φ \to dom F \in dom vol$
11		mbfdm	$⊢ G \in MblFn \to dom G \in dom vol$
12	2 11	syl	$⊢ φ \to dom G \in dom vol$
13		eqid	$⊢ dom F \cap dom G = dom F \cap dom G$
14		eqidd	$⊢ (φ \land x \in dom F) \to F (x) = F (x)$
15		eqidd	$⊢ (φ \land x \in dom G) \to G (x) = G (x)$
16	5 8 10 12 13 14 15	offval	$⊢ φ \to F +_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) + G (x))$
17		elinel1	$⊢ x \in (dom F \cap dom G) \to x \in dom F$
18		ffvelcdm	$⊢ (F : dom F ⟶ ℂ \land x \in dom F) \to F (x) \in ℂ$
19	4 17 18	syl2an	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) \in ℂ$
20		elinel2	$⊢ x \in (dom F \cap dom G) \to x \in dom G$
21		ffvelcdm	$⊢ (G : dom G ⟶ ℂ \land x \in dom G) \to G (x) \in ℂ$
22	7 20 21	syl2an	$⊢ (φ \land x \in (dom F \cap dom G)) \to G (x) \in ℂ$
23	19 22	readdd	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (F (x) + G (x)) = ℜ (F (x)) + ℜ (G (x))$
24	23	mpteq2dva	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x) + G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) + ℜ (G (x)))$
25		inmbl	$⊢ (dom F \in dom vol \land dom G \in dom vol) \to dom F \cap dom G \in dom vol$
26	10 12 25	syl2anc	$⊢ φ \to dom F \cap dom G \in dom vol$
27	19	recld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (F (x)) \in ℝ$
28	22	recld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (G (x)) \in ℝ$
29		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)))$
30		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))$
31	26 27 28 29 30	offval2	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) +_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) + ℜ (G (x)))$
32	24 31	eqtr4d	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x) + G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) +_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))$
33		inss1	$⊢ dom F \cap dom G \subseteq dom F$
34		resmpt	$⊢ dom F \cap dom G \subseteq dom F \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ F (x))$
35	33 34	ax-mp	$⊢ {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ F (x))$
36	4	feqmptd	$⊢ φ \to F = (x \in dom F ⟼ F (x))$
37	36 1	eqeltrrd	$⊢ φ \to (x \in dom F ⟼ F (x)) \in MblFn$
38		mbfres	$⊢ ((x \in dom F ⟼ F (x)) \in MblFn \land dom F \cap dom G \in dom vol) \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
39	37 26 38	syl2anc	$⊢ φ \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
40	35 39	eqeltrrid	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x)) \in MblFn$
41	19	ismbfcn2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ F (x)) \in MblFn \leftrightarrow ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \in MblFn))$
42	40 41	mpbid	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \in MblFn)$
43	42	simpld	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \in MblFn$
44		inss2	$⊢ dom F \cap dom G \subseteq dom G$
45		resmpt	$⊢ dom F \cap dom G \subseteq dom G \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ G (x))$
46	44 45	ax-mp	$⊢ {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ G (x))$
47	7	feqmptd	$⊢ φ \to G = (x \in dom G ⟼ G (x))$
48	47 2	eqeltrrd	$⊢ φ \to (x \in dom G ⟼ G (x)) \in MblFn$
49		mbfres	$⊢ ((x \in dom G ⟼ G (x)) \in MblFn \land dom F \cap dom G \in dom vol) \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
50	48 26 49	syl2anc	$⊢ φ \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
51	46 50	eqeltrrid	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ G (x)) \in MblFn$
52	22	ismbfcn2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ G (x)) \in MblFn \leftrightarrow ((x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn))$
53	51 52	mpbid	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn)$
54	53	simpld	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn$
55	27	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) : dom F \cap dom G ⟶ ℝ$
56	28	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) : dom F \cap dom G ⟶ ℝ$
57	43 54 55 56	mbfaddlem	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) +_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn$
58	32 57	eqeltrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x) + G (x))) \in MblFn$
59	19 22	imaddd	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (F (x) + G (x)) = ℑ (F (x)) + ℑ (G (x))$
60	59	mpteq2dva	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x) + G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x)) + ℑ (G (x)))$
61	19	imcld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (F (x)) \in ℝ$
62	22	imcld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (G (x)) \in ℝ$
63		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x)))$
64		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))$
65	26 61 62 63 64	offval2	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) +_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x)) + ℑ (G (x)))$
66	60 65	eqtr4d	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x) + G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) +_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))$
67	42	simprd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \in MblFn$
68	53	simprd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn$
69	61	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) : dom F \cap dom G ⟶ ℝ$
70	62	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) : dom F \cap dom G ⟶ ℝ$
71	67 68 69 70	mbfaddlem	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) +_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn$
72	66 71	eqeltrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x) + G (x))) \in MblFn$
73	19 22	addcld	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) + G (x) \in ℂ$
74	73	ismbfcn2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ F (x) + G (x)) \in MblFn \leftrightarrow ((x \in (dom F \cap dom G) ⟼ ℜ (F (x) + G (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (F (x) + G (x))) \in MblFn))$
75	58 72 74	mpbir2and	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x) + G (x)) \in MblFn$
76	16 75	eqeltrd	$⊢ φ \to F +_{f} G \in MblFn$

Metamath Proof Explorer

Theorem mbfadd

Proof