smfmul

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

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

Proof

Step	Hyp	Ref	Expression
1		smfmul.x	$⊢ Ⅎ x φ$
2		smfmul.s	$⊢ φ \to S \in SAlg$
3		smfmul.a	$⊢ φ \to A \in V$
4		smfmul.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfmul.d	$⊢ (φ \land x \in C) \to D \in ℝ$
6		smfmul.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
7		smfmul.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	remulcld	$⊢ (φ \land x \in (A \cap C)) \to B D \in ℝ$
24		nfv	$⊢ Ⅎ x a \in ℝ$
25	1 24	nfan	$⊢ Ⅎ x (φ \land a \in ℝ)$
26	2	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
27	3	adantr	$⊢ (φ \land a \in ℝ) \to A \in V$
28	4	adantlr	$⊢ ((φ \land a \in ℝ) \land x \in A) \to B \in ℝ$
29	5	adantlr	$⊢ ((φ \land a \in ℝ) \land x \in C) \to D \in ℝ$
30	6	adantr	$⊢ (φ \land a \in ℝ) \to (x \in A ⟼ B) \in SMblFn (S)$
31	7	adantr	$⊢ (φ \land a \in ℝ) \to (x \in C ⟼ D) \in SMblFn (S)$
32		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
33		fveq1	$⊢ p = q \to p (2) = q (2)$
34		fveq1	$⊢ p = q \to p (3) = q (3)$
35	33 34	oveq12d	$⊢ p = q \to (p (2), p (3)) = (q (2), q (3))$
36	35	raleqdv	$⊢ p = q \to (\forall v \in (p (2), p (3)) u v < a \leftrightarrow \forall v \in (q (2), q (3)) u v < a)$
37	36	ralbidv	$⊢ p = q \to (\forall u \in (p (0), p (1)) \forall v \in (p (2), p (3)) u v < a \leftrightarrow \forall u \in (p (0), p (1)) \forall v \in (q (2), q (3)) u v < a)$
38		fveq1	$⊢ p = q \to p (0) = q (0)$
39		fveq1	$⊢ p = q \to p (1) = q (1)$
40	38 39	oveq12d	$⊢ p = q \to (p (0), p (1)) = (q (0), q (1))$
41	40	raleqdv	$⊢ p = q \to (\forall u \in (p (0), p (1)) \forall v \in (q (2), q (3)) u v < a \leftrightarrow \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < a)$
42	37 41	bitrd	$⊢ p = q \to (\forall u \in (p (0), p (1)) \forall v \in (p (2), p (3)) u v < a \leftrightarrow \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < a)$
43	42	cbvrabv	$⊢ \{p \in (ℚ^{(0 \dots 3)}) \| \forall u \in (p (0), p (1)) \forall v \in (p (2), p (3)) u v < a\} = \{q \in (ℚ^{(0 \dots 3)}) \| \forall u \in (q (0), q (1)) \forall v \in (q (2), q (3)) u v < a\}$
44		eqid	$⊢ (q \in \{p \in (ℚ^{(0 \dots 3)}) \| \forall u \in (p (0), p (1)) \forall v \in (p (2), p (3)) u v < a\} ⟼ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\}) = (q \in \{p \in (ℚ^{(0 \dots 3)}) \| \forall u \in (p (0), p (1)) \forall v \in (p (2), p (3)) u v < a\} ⟼ \{x \in (A \cap C) \| (B \in (q (0), q (1)) \land D \in (q (2), q (3)))\})$
45	25 26 27 28 29 30 31 32 43 44	smfmullem4	$⊢ (φ \land a \in ℝ) \to \{x \in (A \cap C) \| B D < a\} \in (S ↾_{𝑡} (A \cap C))$
46	1 8 2 18 23 45	issmfdmpt	$⊢ φ \to (x \in (A \cap C) ⟼ B D) \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfmul

Proof