Theorem smfdivdmmbl

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 needed only for the function at the denominator). (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	smfdivdmmbl.1	$$⊢Ⅎx\phi$$
	smfdivdmmbl.2	$$⊢\underset{\_}{Ⅎ}xB$$
	smfdivdmmbl.3	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfdivdmmbl.4	$$⊢\phi \to A\in S$$
	smfdivdmmbl.5	$$⊢\phi \to B\in S$$
	smfdivdmmbl.6	$$⊢\left(\phi \wedge x\in B\right)\to D\in W$$
	smfdivdmmbl.7	$$⊢\phi \to \left(x\in B⟼D\right)\in \mathrm{SMblFn}\left(S\right)$$
	smfdivdmmbl.8	$$⊢E=\left\{x\in B|D\ne 0\right\}$$
Assertion	smfdivdmmbl	$$⊢\phi \to A\cap E\in S$$

Proof

Step	Hyp	Ref	Expression
1		smfdivdmmbl.1	$$⊢Ⅎx\phi$$
2		smfdivdmmbl.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		smfdivdmmbl.3	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		smfdivdmmbl.4	$$⊢\phi \to A\in S$$
5		smfdivdmmbl.5	$$⊢\phi \to B\in S$$
6		smfdivdmmbl.6	$$⊢\left(\phi \wedge x\in B\right)\to D\in W$$
7		smfdivdmmbl.7	$$⊢\phi \to \left(x\in B⟼D\right)\in \mathrm{SMblFn}\left(S\right)$$
8		smfdivdmmbl.8	$$⊢E=\left\{x\in B|D\ne 0\right\}$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xℝ$$
10	1 2 3 6 7	smffmptf	$$⊢\phi \to \left(x\in B⟼D\right):B⟶ℝ$$
11	2 9 10	fvmptelcdmf	$$⊢\left(\phi \wedge x\in B\right)\to D\in ℝ$$
12		0red	$$⊢\phi \to 0\in ℝ$$
13	1 2 3 5 11 7 12 8	smfdmmblpimne	$$⊢\phi \to E\in S$$
14	3 4 13	salincld	$$⊢\phi \to A\cap E\in S$$