smfdiv

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

	Ref	Expression
Hypotheses	smfdiv.x	$⊢ Ⅎ x φ$
	smfdiv.s	$⊢ φ \to S \in SAlg$
	smfdiv.a	$⊢ φ \to A \in V$
	smfdiv.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfdiv.c	$⊢ φ \to C \in W$
	smfdiv.d	$⊢ (φ \land x \in C) \to D \in ℝ$
	smfdiv.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
	smfdiv.n	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
	smfdiv.e	$⊢ E = \{x \in C \| D \neq 0\}$
Assertion	smfdiv	$⊢ φ \to (x \in (A \cap E) ⟼ \frac{B}{D}) \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfdiv.x	$⊢ Ⅎ x φ$
2		smfdiv.s	$⊢ φ \to S \in SAlg$
3		smfdiv.a	$⊢ φ \to A \in V$
4		smfdiv.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfdiv.c	$⊢ φ \to C \in W$
6		smfdiv.d	$⊢ (φ \land x \in C) \to D \in ℝ$
7		smfdiv.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
8		smfdiv.n	$⊢ φ \to (x \in C ⟼ D) \in SMblFn (S)$
9		smfdiv.e	$⊢ E = \{x \in C \| D \neq 0\}$
10		elinel1	$⊢ x \in (A \cap E) \to x \in A$
11	10	adantl	$⊢ (φ \land x \in (A \cap E)) \to x \in A$
12	11 4	syldan	$⊢ (φ \land x \in (A \cap E)) \to B \in ℝ$
13	12	recnd	$⊢ (φ \land x \in (A \cap E)) \to B \in ℂ$
14		ssrab2	$⊢ \{x \in C \| D \neq 0\} \subseteq C$
15	9 14	eqsstri	$⊢ E \subseteq C$
16		elinel2	$⊢ x \in (A \cap E) \to x \in E$
17	15 16	sseldi	$⊢ x \in (A \cap E) \to x \in C$
18	17	adantl	$⊢ (φ \land x \in (A \cap E)) \to x \in C$
19	18 6	syldan	$⊢ (φ \land x \in (A \cap E)) \to D \in ℝ$
20	19	recnd	$⊢ (φ \land x \in (A \cap E)) \to D \in ℂ$
21	9	eleq2i	$⊢ x \in E \leftrightarrow x \in \{x \in C \| D \neq 0\}$
22	21	biimpi	$⊢ x \in E \to x \in \{x \in C \| D \neq 0\}$
23		rabidim2	$⊢ x \in \{x \in C \| D \neq 0\} \to D \neq 0$
24	22 23	syl	$⊢ x \in E \to D \neq 0$
25	16 24	syl	$⊢ x \in (A \cap E) \to D \neq 0$
26	25	adantl	$⊢ (φ \land x \in (A \cap E)) \to D \neq 0$
27	13 20 26	divrecd	$⊢ (φ \land x \in (A \cap E)) \to \frac{B}{D} = B (\frac{1}{D})$
28	1 27	mpteq2da	$⊢ φ \to (x \in (A \cap E) ⟼ \frac{B}{D}) = (x \in (A \cap E) ⟼ B (\frac{1}{D}))$
29		1red	$⊢ (φ \land x \in E) \to 1 \in ℝ$
30	15	sseli	$⊢ x \in E \to x \in C$
31	30	adantl	$⊢ (φ \land x \in E) \to x \in C$
32	31 6	syldan	$⊢ (φ \land x \in E) \to D \in ℝ$
33	24	adantl	$⊢ (φ \land x \in E) \to D \neq 0$
34	29 32 33	redivcld	$⊢ (φ \land x \in E) \to \frac{1}{D} \in ℝ$
35	1 2 5 6 8 9	smfrec	$⊢ φ \to (x \in E ⟼ \frac{1}{D}) \in SMblFn (S)$
36	1 2 3 4 34 7 35	smfmul	$⊢ φ \to (x \in (A \cap E) ⟼ B (\frac{1}{D})) \in SMblFn (S)$
37	28 36	eqeltrd	$⊢ φ \to (x \in (A \cap E) ⟼ \frac{B}{D}) \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfdiv

Proof