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	|- F/ x ph
	smfdivdmmbl.2	|- F/_ x B
	smfdivdmmbl.3	|- ( ph -> S e. SAlg )
	smfdivdmmbl.4	|- ( ph -> A e. S )
	smfdivdmmbl.5	|- ( ph -> B e. S )
	smfdivdmmbl.6	|- ( ( ph /\ x e. B ) -> D e. W )
	smfdivdmmbl.7	|- ( ph -> ( x e. B |-> D ) e. ( SMblFn ` S ) )
	smfdivdmmbl.8	|- E = { x e. B | D =/= 0 }
Assertion	smfdivdmmbl	|- ( ph -> ( A i^i E ) e. S )

Proof

Step	Hyp	Ref	Expression
1		smfdivdmmbl.1	|- F/ x ph
2		smfdivdmmbl.2	|- F/_ x B
3		smfdivdmmbl.3	|- ( ph -> S e. SAlg )
4		smfdivdmmbl.4	|- ( ph -> A e. S )
5		smfdivdmmbl.5	|- ( ph -> B e. S )
6		smfdivdmmbl.6	|- ( ( ph /\ x e. B ) -> D e. W )
7		smfdivdmmbl.7	|- ( ph -> ( x e. B |-> D ) e. ( SMblFn ` S ) )
8		smfdivdmmbl.8	|- E = { x e. B | D =/= 0 }
9		nfcv	|- F/_ x RR
10	1 2 3 6 7	smffmptf	|- ( ph -> ( x e. B |-> D ) : B --> RR )
11	2 9 10	fvmptelcdmf	|- ( ( ph /\ x e. B ) -> D e. RR )
12		0red	|- ( ph -> 0 e. RR )
13	1 2 3 5 11 7 12 8	smfdmmblpimne	|- ( ph -> E e. S )
14	3 4 13	salincld	|- ( ph -> ( A i^i E ) e. S )