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	|- F/ x ph
	smfdivdmmbl2.2	|- F/_ x F
	smfdivdmmbl2.3	|- F/_ x G
	smfdivdmmbl2.4	|- ( ph -> S e. SAlg )
	smfdivdmmbl2.5	|- ( ph -> F : A --> V )
	smfdivdmmbl2.6	|- ( ph -> G e. ( SMblFn ` S ) )
	smfdivdmmbl2.7	|- ( ph -> A e. S )
	smfdivdmmbl2.8	|- ( ph -> dom G e. S )
	smfdivdmmbl2.9	|- D = { x e. dom G | ( G ` x ) =/= 0 }
	smfdivdmmbl2.10	|- H = ( x e. ( dom F i^i D ) |-> ( ( F ` x ) / ( G ` x ) ) )
Assertion	smfdivdmmbl2	|- ( ph -> dom H e. S )

Proof

Step	Hyp	Ref	Expression
1		smfdivdmmbl2.1	|- F/ x ph
2		smfdivdmmbl2.2	|- F/_ x F
3		smfdivdmmbl2.3	|- F/_ x G
4		smfdivdmmbl2.4	|- ( ph -> S e. SAlg )
5		smfdivdmmbl2.5	|- ( ph -> F : A --> V )
6		smfdivdmmbl2.6	|- ( ph -> G e. ( SMblFn ` S ) )
7		smfdivdmmbl2.7	|- ( ph -> A e. S )
8		smfdivdmmbl2.8	|- ( ph -> dom G e. S )
9		smfdivdmmbl2.9	|- D = { x e. dom G | ( G ` x ) =/= 0 }
10		smfdivdmmbl2.10	|- H = ( x e. ( dom F i^i D ) |-> ( ( F ` x ) / ( G ` x ) ) )
11	2	nfdm	|- F/_ x dom F
12		nfrab1	|- F/_ x { x e. dom G | ( G ` x ) =/= 0 }
13	9 12	nfcxfr	|- F/_ x D
14	11 13	nfin	|- F/_ x ( dom F i^i D )
15		ovex	|- ( ( F ` x ) / ( G ` x ) ) e. _V
16	14 15 10	dmmptif	|- dom H = ( dom F i^i D )
17	5	fdmd	|- ( ph -> dom F = A )
18	17 7	eqeltrd	|- ( ph -> dom F e. S )
19	4 8	salrestss	|- ( ph -> ( S |`t dom G ) C_ S )
20		eqid	|- dom G = dom G
21	1 3 4 6 20	smfpimne2	|- ( ph -> { x e. dom G | ( G ` x ) =/= 0 } e. ( S |`t dom G ) )
22	9 21	eqeltrid	|- ( ph -> D e. ( S |`t dom G ) )
23	19 22	sseldd	|- ( ph -> D e. S )
24	4 18 23	salincld	|- ( ph -> ( dom F i^i D ) e. S )
25	16 24	eqeltrid	|- ( ph -> dom H e. S )