Theorem smfdivdmmbl2

Description: If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of Fremlin1 p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator. It is required only for the function at the denominator. (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	smfdivdmmbl2.1	$$⊢Ⅎx\phi$$
	smfdivdmmbl2.2	$$⊢\underset{\_}{Ⅎ}xF$$
	smfdivdmmbl2.3	$$⊢\underset{\_}{Ⅎ}xG$$
	smfdivdmmbl2.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfdivdmmbl2.5	$$⊢\phi \to F:A⟶V$$
	smfdivdmmbl2.6	$$⊢\phi \to G\in \mathrm{SMblFn}\left(S\right)$$
	smfdivdmmbl2.7	$$⊢\phi \to A\in S$$
	smfdivdmmbl2.8	$$⊢\phi \to \mathrm{dom}G\in S$$
	smfdivdmmbl2.9	$$⊢D=\left\{x\in \mathrm{dom}G|G\left(x\right)\ne 0\right\}$$
	smfdivdmmbl2.10	$$⊢H=\left(x\in \left(\mathrm{dom}F\cap D\right)⟼\frac{F\left(x\right)}{G\left(x\right)}\right)$$
Assertion	smfdivdmmbl2	$$⊢\phi \to \mathrm{dom}H\in S$$

Proof

Step	Hyp	Ref	Expression
1		smfdivdmmbl2.1	$$⊢Ⅎx\phi$$
2		smfdivdmmbl2.2	$$⊢\underset{\_}{Ⅎ}xF$$
3		smfdivdmmbl2.3	$$⊢\underset{\_}{Ⅎ}xG$$
4		smfdivdmmbl2.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
5		smfdivdmmbl2.5	$$⊢\phi \to F:A⟶V$$
6		smfdivdmmbl2.6	$$⊢\phi \to G\in \mathrm{SMblFn}\left(S\right)$$
7		smfdivdmmbl2.7	$$⊢\phi \to A\in S$$
8		smfdivdmmbl2.8	$$⊢\phi \to \mathrm{dom}G\in S$$
9		smfdivdmmbl2.9	$$⊢D=\left\{x\in \mathrm{dom}G|G\left(x\right)\ne 0\right\}$$
10		smfdivdmmbl2.10	$$⊢H=\left(x\in \left(\mathrm{dom}F\cap D\right)⟼\frac{F\left(x\right)}{G\left(x\right)}\right)$$
11	2	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}F$$
12		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in \mathrm{dom}G|G\left(x\right)\ne 0\right\}$$
13	9 12	nfcxfr	$$⊢\underset{\_}{Ⅎ}xD$$
14	11 13	nfin	$$⊢\underset{\_}{Ⅎ}x\left(\mathrm{dom}F\cap D\right)$$
15		ovex	$$⊢\frac{F\left(x\right)}{G\left(x\right)}\in \mathrm{V}$$
16	14 15 10	dmmptif	$$⊢\mathrm{dom}H=\mathrm{dom}F\cap D$$
17	5	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
18	17 7	eqeltrd	$$⊢\phi \to \mathrm{dom}F\in S$$
19	4 8	salrestss	$$⊢\phi \to S{\upharpoonright }_{𝑡}\mathrm{dom}G\subseteq S$$
20		eqid	$$⊢\mathrm{dom}G=\mathrm{dom}G$$
21	1 3 4 6 20	smfpimne2	$$⊢\phi \to \left\{x\in \mathrm{dom}G|G\left(x\right)\ne 0\right\}\in \left(S{\upharpoonright }_{𝑡}\mathrm{dom}G\right)$$
22	9 21	eqeltrid	$$⊢\phi \to D\in \left(S{\upharpoonright }_{𝑡}\mathrm{dom}G\right)$$
23	19 22	sseldd	$$⊢\phi \to D\in S$$
24	4 18 23	salincld	$$⊢\phi \to \mathrm{dom}F\cap D\in S$$
25	16 24	eqeltrid	$$⊢\phi \to \mathrm{dom}H\in S$$