mbfsub

Description: The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014)

	Ref	Expression
Hypotheses	mbfadd.1	$⊢ φ \to F \in MblFn$
	mbfadd.2	$⊢ φ \to G \in MblFn$
Assertion	mbfsub	$⊢ φ \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		elinel1	$⊢ x \in (dom F \cap dom G) \to x \in dom F$
6		ffvelcdm	$⊢ (F : dom F ⟶ ℂ \land x \in dom F) \to F (x) \in ℂ$
7	4 5 6	syl2an	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) \in ℂ$
8		mbff	$⊢ G \in MblFn \to G : dom G ⟶ ℂ$
9	2 8	syl	$⊢ φ \to G : dom G ⟶ ℂ$
10		elinel2	$⊢ x \in (dom F \cap dom G) \to x \in dom G$
11		ffvelcdm	$⊢ (G : dom G ⟶ ℂ \land x \in dom G) \to G (x) \in ℂ$
12	9 10 11	syl2an	$⊢ (φ \land x \in (dom F \cap dom G)) \to G (x) \in ℂ$
13	7 12	negsubd	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) + (- G (x)) = F (x) - G (x)$
14	13	eqcomd	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) - G (x) = F (x) + (- G (x))$
15	14	mpteq2dva	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x) - G (x)) = (x \in (dom F \cap dom G) ⟼ F (x) + (- G (x)))$
16	4	ffnd	$⊢ φ \to F Fn dom F$
17	9	ffnd	$⊢ φ \to G Fn dom G$
18		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
19	1 18	syl	$⊢ φ \to dom F \in dom vol$
20		mbfdm	$⊢ G \in MblFn \to dom G \in dom vol$
21	2 20	syl	$⊢ φ \to dom G \in dom vol$
22		eqid	$⊢ dom F \cap dom G = dom F \cap dom G$
23		eqidd	$⊢ (φ \land x \in dom F) \to F (x) = F (x)$
24		eqidd	$⊢ (φ \land x \in dom G) \to G (x) = G (x)$
25	16 17 19 21 22 23 24	offval	$⊢ φ \to F -_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) - G (x))$
26		inmbl	$⊢ (dom F \in dom vol \land dom G \in dom vol) \to dom F \cap dom G \in dom vol$
27	19 21 26	syl2anc	$⊢ φ \to dom F \cap dom G \in dom vol$
28	12	negcld	$⊢ (φ \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	27 7 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	15 25 31	3eqtr4d	$⊢ φ \to F -_{f} G = (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	mp1i	$⊢ φ \to {(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 27 38	syl2anc	$⊢ φ \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
40	35 39	eqeltrrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x)) \in MblFn$
41		inss2	$⊢ dom F \cap dom G \subseteq dom G$
42		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))$
43	41 42	mp1i	$⊢ φ \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ G (x))$
44	9	feqmptd	$⊢ φ \to G = (x \in dom G ⟼ G (x))$
45	44 2	eqeltrrd	$⊢ φ \to (x \in dom G ⟼ G (x)) \in MblFn$
46		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$
47	45 27 46	syl2anc	$⊢ φ \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
48	43 47	eqeltrrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ G (x)) \in MblFn$
49	12 48	mbfneg	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ - G (x)) \in MblFn$
50	40 49	mbfadd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x)) +_{f} (x \in (dom F \cap dom G) ⟼ - G (x)) \in MblFn$
51	32 50	eqeltrd	$⊢ φ \to F -_{f} G \in MblFn$

Metamath Proof Explorer

Theorem mbfsub

Proof