mbfaddlem

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$
	mbfadd.3	$⊢ φ \to F : A ⟶ ℝ$
	mbfadd.4	$⊢ φ \to G : A ⟶ ℝ$
Assertion	mbfaddlem	$⊢ φ \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		mbfadd.3	$⊢ φ \to F : A ⟶ ℝ$
4		mbfadd.4	$⊢ φ \to G : A ⟶ ℝ$
5		readdcl	$⊢ (x \in ℝ \land y \in ℝ) \to x + y \in ℝ$
6	5	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x + y \in ℝ$
7	3	fdmd	$⊢ φ \to dom F = A$
8		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
9	1 8	syl	$⊢ φ \to dom F \in dom vol$
10	7 9	eqeltrrd	$⊢ φ \to A \in dom vol$
11		inidm	$⊢ A \cap A = A$
12	6 3 4 10 10 11	off	$⊢ φ \to (F +_{f} G) : A ⟶ ℝ$
13		eliun	$⊢ x \in ⋃_{r \in ℚ} (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \leftrightarrow \exists r \in ℚ x \in (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)])$
14		r19.42v	$⊢ \exists r \in ℚ (x \in A \land (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞))) \leftrightarrow (x \in A \land \exists r \in ℚ (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞)))$
15		simplr	$⊢ ((φ \land y \in ℝ) \land x \in A) \to y \in ℝ$
16	4	adantr	$⊢ (φ \land y \in ℝ) \to G : A ⟶ ℝ$
17	16	ffvelcdmda	$⊢ ((φ \land y \in ℝ) \land x \in A) \to G (x) \in ℝ$
18	3	adantr	$⊢ (φ \land y \in ℝ) \to F : A ⟶ ℝ$
19	18	ffvelcdmda	$⊢ ((φ \land y \in ℝ) \land x \in A) \to F (x) \in ℝ$
20	15 17 19	ltsubaddd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y - G (x) < F (x) \leftrightarrow y < F (x) + G (x))$
21	15	adantr	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to y \in ℝ$
22		qre	$⊢ r \in ℚ \to r \in ℝ$
23	22	adantl	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to r \in ℝ$
24	17	adantr	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to G (x) \in ℝ$
25		ltsub23	$⊢ (y \in ℝ \land r \in ℝ \land G (x) \in ℝ) \to (y - r < G (x) \leftrightarrow y - G (x) < r)$
26	21 23 24 25	syl3anc	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to (y - r < G (x) \leftrightarrow y - G (x) < r)$
27	26	anbi1cd	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to ((r < F (x) \land y - r < G (x)) \leftrightarrow (y - G (x) < r \land r < F (x)))$
28	27	rexbidva	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (r < F (x) \land y - r < G (x)) \leftrightarrow \exists r \in ℚ (y - G (x) < r \land r < F (x)))$
29	15 17	resubcld	$⊢ ((φ \land y \in ℝ) \land x \in A) \to y - G (x) \in ℝ$
30	29	adantr	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to y - G (x) \in ℝ$
31	19	adantr	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to F (x) \in ℝ$
32		lttr	$⊢ (y - G (x) \in ℝ \land r \in ℝ \land F (x) \in ℝ) \to ((y - G (x) < r \land r < F (x)) \to y - G (x) < F (x))$
33	30 23 31 32	syl3anc	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to ((y - G (x) < r \land r < F (x)) \to y - G (x) < F (x))$
34	33	rexlimdva	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (y - G (x) < r \land r < F (x)) \to y - G (x) < F (x))$
35		qbtwnre	$⊢ (y - G (x) \in ℝ \land F (x) \in ℝ \land y - G (x) < F (x)) \to \exists r \in ℚ (y - G (x) < r \land r < F (x))$
36	35	3expia	$⊢ (y - G (x) \in ℝ \land F (x) \in ℝ) \to (y - G (x) < F (x) \to \exists r \in ℚ (y - G (x) < r \land r < F (x)))$
37	29 19 36	syl2anc	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y - G (x) < F (x) \to \exists r \in ℚ (y - G (x) < r \land r < F (x)))$
38	34 37	impbid	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (y - G (x) < r \land r < F (x)) \leftrightarrow y - G (x) < F (x))$
39	28 38	bitrd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (r < F (x) \land y - r < G (x)) \leftrightarrow y - G (x) < F (x))$
40	3	ffnd	$⊢ φ \to F Fn A$
41	40	adantr	$⊢ (φ \land y \in ℝ) \to F Fn A$
42	4	ffnd	$⊢ φ \to G Fn A$
43	42	adantr	$⊢ (φ \land y \in ℝ) \to G Fn A$
44	10	adantr	$⊢ (φ \land y \in ℝ) \to A \in dom vol$
45		eqidd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to F (x) = F (x)$
46		eqidd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to G (x) = G (x)$
47	41 43 44 44 11 45 46	ofval	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F +_{f} G) (x) = F (x) + G (x)$
48	47	breq2d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (y < (F +_{f} G) (x) \leftrightarrow y < F (x) + G (x))$
49	20 39 48	3bitr4d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (r < F (x) \land y - r < G (x)) \leftrightarrow y < (F +_{f} G) (x))$
50	23	rexrd	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to r \in ℝ^{*}$
51		elioopnf	$⊢ r \in ℝ^{*} \to (F (x) \in (r, +∞) \leftrightarrow (F (x) \in ℝ \land r < F (x)))$
52	50 51	syl	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to (F (x) \in (r, +∞) \leftrightarrow (F (x) \in ℝ \land r < F (x)))$
53	31 52	mpbirand	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to (F (x) \in (r, +∞) \leftrightarrow r < F (x))$
54	21 23	resubcld	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to y - r \in ℝ$
55	54	rexrd	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to y - r \in ℝ^{*}$
56		elioopnf	$⊢ y - r \in ℝ^{*} \to (G (x) \in (y - r, +∞) \leftrightarrow (G (x) \in ℝ \land y - r < G (x)))$
57	55 56	syl	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to (G (x) \in (y - r, +∞) \leftrightarrow (G (x) \in ℝ \land y - r < G (x)))$
58	24 57	mpbirand	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to (G (x) \in (y - r, +∞) \leftrightarrow y - r < G (x))$
59	53 58	anbi12d	$⊢ (((φ \land y \in ℝ) \land x \in A) \land r \in ℚ) \to ((F (x) \in (r, +∞) \land G (x) \in (y - r, +∞)) \leftrightarrow (r < F (x) \land y - r < G (x)))$
60	59	rexbidva	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞)) \leftrightarrow \exists r \in ℚ (r < F (x) \land y - r < G (x)))$
61	12	adantr	$⊢ (φ \land y \in ℝ) \to (F +_{f} G) : A ⟶ ℝ$
62	61	ffvelcdmda	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (F +_{f} G) (x) \in ℝ$
63	15	rexrd	$⊢ ((φ \land y \in ℝ) \land x \in A) \to y \in ℝ^{*}$
64		elioopnf	$⊢ y \in ℝ^{*} \to ((F +_{f} G) (x) \in (y, +∞) \leftrightarrow ((F +_{f} G) (x) \in ℝ \land y < (F +_{f} G) (x)))$
65	63 64	syl	$⊢ ((φ \land y \in ℝ) \land x \in A) \to ((F +_{f} G) (x) \in (y, +∞) \leftrightarrow ((F +_{f} G) (x) \in ℝ \land y < (F +_{f} G) (x)))$
66	62 65	mpbirand	$⊢ ((φ \land y \in ℝ) \land x \in A) \to ((F +_{f} G) (x) \in (y, +∞) \leftrightarrow y < (F +_{f} G) (x))$
67	49 60 66	3bitr4d	$⊢ ((φ \land y \in ℝ) \land x \in A) \to (\exists r \in ℚ (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞)) \leftrightarrow (F +_{f} G) (x) \in (y, +∞))$
68	67	pm5.32da	$⊢ (φ \land y \in ℝ) \to ((x \in A \land \exists r \in ℚ (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞))) \leftrightarrow (x \in A \land (F +_{f} G) (x) \in (y, +∞)))$
69	14 68	bitrid	$⊢ (φ \land y \in ℝ) \to (\exists r \in ℚ (x \in A \land (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞))) \leftrightarrow (x \in A \land (F +_{f} G) (x) \in (y, +∞)))$
70		elpreima	$⊢ F Fn A \to (x \in F^{-1} [(r, +∞)] \leftrightarrow (x \in A \land F (x) \in (r, +∞)))$
71	41 70	syl	$⊢ (φ \land y \in ℝ) \to (x \in F^{-1} [(r, +∞)] \leftrightarrow (x \in A \land F (x) \in (r, +∞)))$
72		elpreima	$⊢ G Fn A \to (x \in G^{-1} [(y - r, +∞)] \leftrightarrow (x \in A \land G (x) \in (y - r, +∞)))$
73	43 72	syl	$⊢ (φ \land y \in ℝ) \to (x \in G^{-1} [(y - r, +∞)] \leftrightarrow (x \in A \land G (x) \in (y - r, +∞)))$
74	71 73	anbi12d	$⊢ (φ \land y \in ℝ) \to ((x \in F^{-1} [(r, +∞)] \land x \in G^{-1} [(y - r, +∞)]) \leftrightarrow ((x \in A \land F (x) \in (r, +∞)) \land (x \in A \land G (x) \in (y - r, +∞))))$
75		elin	$⊢ x \in (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \leftrightarrow (x \in F^{-1} [(r, +∞)] \land x \in G^{-1} [(y - r, +∞)])$
76		anandi	$⊢ (x \in A \land (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞))) \leftrightarrow ((x \in A \land F (x) \in (r, +∞)) \land (x \in A \land G (x) \in (y - r, +∞)))$
77	74 75 76	3bitr4g	$⊢ (φ \land y \in ℝ) \to (x \in (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \leftrightarrow (x \in A \land (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞))))$
78	77	rexbidv	$⊢ (φ \land y \in ℝ) \to (\exists r \in ℚ x \in (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \leftrightarrow \exists r \in ℚ (x \in A \land (F (x) \in (r, +∞) \land G (x) \in (y - r, +∞))))$
79	12	ffnd	$⊢ φ \to (F +_{f} G) Fn A$
80	79	adantr	$⊢ (φ \land y \in ℝ) \to (F +_{f} G) Fn A$
81		elpreima	$⊢ (F +_{f} G) Fn A \to (x \in {(F +_{f} G)}^{-1} [(y, +∞)] \leftrightarrow (x \in A \land (F +_{f} G) (x) \in (y, +∞)))$
82	80 81	syl	$⊢ (φ \land y \in ℝ) \to (x \in {(F +_{f} G)}^{-1} [(y, +∞)] \leftrightarrow (x \in A \land (F +_{f} G) (x) \in (y, +∞)))$
83	69 78 82	3bitr4d	$⊢ (φ \land y \in ℝ) \to (\exists r \in ℚ x \in (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \leftrightarrow x \in {(F +_{f} G)}^{-1} [(y, +∞)])$
84	13 83	bitrid	$⊢ (φ \land y \in ℝ) \to (x \in ⋃_{r \in ℚ} (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \leftrightarrow x \in {(F +_{f} G)}^{-1} [(y, +∞)])$
85	84	eqrdv	$⊢ (φ \land y \in ℝ) \to ⋃_{r \in ℚ} (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) = {(F +_{f} G)}^{-1} [(y, +∞)]$
86		qnnen	$⊢ ℚ \approx ℕ$
87		endom	$⊢ ℚ \approx ℕ \to ℚ ≼ ℕ$
88	86 87	ax-mp	$⊢ ℚ ≼ ℕ$
89		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(r, +∞)] \in dom vol$
90	1 3 89	syl2anc	$⊢ φ \to F^{-1} [(r, +∞)] \in dom vol$
91		mbfima	$⊢ (G \in MblFn \land G : A ⟶ ℝ) \to G^{-1} [(y - r, +∞)] \in dom vol$
92	2 4 91	syl2anc	$⊢ φ \to G^{-1} [(y - r, +∞)] \in dom vol$
93		inmbl	$⊢ (F^{-1} [(r, +∞)] \in dom vol \land G^{-1} [(y - r, +∞)] \in dom vol) \to F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)] \in dom vol$
94	90 92 93	syl2anc	$⊢ φ \to F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)] \in dom vol$
95	94	ad2antrr	$⊢ ((φ \land y \in ℝ) \land r \in ℚ) \to F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)] \in dom vol$
96	95	ralrimiva	$⊢ (φ \land y \in ℝ) \to \forall r \in ℚ F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)] \in dom vol$
97		iunmbl2	$⊢ (ℚ ≼ ℕ \land \forall r \in ℚ F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)] \in dom vol) \to ⋃_{r \in ℚ} (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \in dom vol$
98	88 96 97	sylancr	$⊢ (φ \land y \in ℝ) \to ⋃_{r \in ℚ} (F^{-1} [(r, +∞)] \cap G^{-1} [(y - r, +∞)]) \in dom vol$
99	85 98	eqeltrrd	$⊢ (φ \land y \in ℝ) \to {(F +_{f} G)}^{-1} [(y, +∞)] \in dom vol$
100	12 99	ismbf3d	$⊢ φ \to F +_{f} G \in MblFn$

Metamath Proof Explorer

Theorem mbfaddlem

Proof