smfadd

Description: The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfadd.x	$⊢ Ⅎ x φ$
	smfadd.s	$⊢ φ \to S \in SAlg$
	smfadd.a	$⊢ φ \to A \in V$
	smfadd.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfadd.d	$⊢ (φ \land x \in C) \to D \in ℝ$
	smfadd.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfadd.n	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
Assertion	smfadd	$⊢ φ \to (x \in (A \cap C) ⟼ B + D) \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfadd.x	$⊢ Ⅎ x φ$
2		smfadd.s	$⊢ φ \to S \in SAlg$
3		smfadd.a	$⊢ φ \to A \in V$
4		smfadd.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfadd.d	$⊢ (φ \land x \in C) \to D \in ℝ$
6		smfadd.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
7		smfadd.n	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
8		nfv	$⊢ Ⅎ a φ$
9		elinel1	$⊢ x \in (A \cap C) \to x \in A$
10	9	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in A$
11	1 10	ssdf	$⊢ φ \to A \cap C \subseteq A$
12		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
13	1 12 4	dmmptdf	$⊢ φ \to dom (x \in A ⟼ B) = A$
14	13	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
15		eqid	$⊢ dom (x \in A ⟼ B) = dom (x \in A ⟼ B)$
16	2 6 15	smfdmss	$⊢ φ \to dom (x \in A ⟼ B) \subseteq ⋃ S$
17	14 16	eqsstrd	$⊢ φ \to A \subseteq ⋃ S$
18	11 17	sstrd	$⊢ φ \to A \cap C \subseteq ⋃ S$
19	10 4	syldan	$⊢ (φ \land x \in (A \cap C)) \to B \in ℝ$
20		elinel2	$⊢ x \in (A \cap C) \to x \in C$
21	20	adantl	$⊢ (φ \land x \in (A \cap C)) \to x \in C$
22	21 5	syldan	$⊢ (φ \land x \in (A \cap C)) \to D \in ℝ$
23	19 22	readdcld	$⊢ (φ \land x \in (A \cap C)) \to B + D \in ℝ$
24		eqid	$⊢ (x \in (A \cap C) ⟼ B + D) = (x \in (A \cap C) ⟼ B + D)$
25	1 23 24	fmptdf	$⊢ φ \to (x \in (A \cap C) ⟼ B + D) : A \cap C ⟶ ℝ$
26	25	fvmptelrn	$⊢ (φ \land x \in (A \cap C)) \to B + D \in ℝ$
27		nfv	$⊢ Ⅎ x a \in ℝ$
28	1 27	nfan	$⊢ Ⅎ x (φ \land a \in ℝ)$
29	2	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
30	3	adantr	$⊢ (φ \land a \in ℝ) \to A \in V$
31	4	adantlr	$⊢ ((φ \land a \in ℝ) \land x \in A) \to B \in ℝ$
32	5	adantlr	$⊢ ((φ \land a \in ℝ) \land x \in C) \to D \in ℝ$
33	6	adantr	$⊢ (φ \land a \in ℝ) \to (x \in A ⟼ B) \in SMblFn (S)$
34	7	adantr	$⊢ (φ \land a \in ℝ) \to (x \in C ⟼ D) \in SMblFn (S)$
35		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
36		oveq2	$⊢ r = q \to p + r = p + q$
37	36	breq1d	$⊢ r = q \to (p + r < a \leftrightarrow p + q < a)$
38	37	cbvrabv	$⊢ \{r \in ℚ \| p + r < a\} = \{q \in ℚ \| p + q < a\}$
39	38	mpteq2i	$⊢ (p \in ℚ ⟼ \{r \in ℚ \| p + r < a\}) = (p \in ℚ ⟼ \{q \in ℚ \| p + q < a\})$
40	28 29 30 31 32 33 34 35 39	smfaddlem2	$⊢ (φ \land a \in ℝ) \to \{x \in (A \cap C) \| B + D < a\} \in (S ↾_{𝑡} (A \cap C))$
41	1 8 2 18 26 40	issmfdmpt	$⊢ φ \to (x \in (A \cap C) ⟼ B + D) \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfadd

Proof