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	⊢ Ⅎ 𝑥 𝜑
	smfdivdmmbl2.2	⊢ Ⅎ 𝑥 𝐹
	smfdivdmmbl2.3	⊢ Ⅎ 𝑥 𝐺
	smfdivdmmbl2.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfdivdmmbl2.5	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑉 )
	smfdivdmmbl2.6	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )
	smfdivdmmbl2.7	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	smfdivdmmbl2.8	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )
	smfdivdmmbl2.9	⊢ 𝐷 = { 𝑥 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 }
	smfdivdmmbl2.10	⊢ 𝐻 = ( 𝑥 ∈ ( dom 𝐹 ∩ 𝐷 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
Assertion	smfdivdmmbl2	⊢ ( 𝜑 → dom 𝐻 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		smfdivdmmbl2.1	⊢ Ⅎ 𝑥 𝜑
2		smfdivdmmbl2.2	⊢ Ⅎ 𝑥 𝐹
3		smfdivdmmbl2.3	⊢ Ⅎ 𝑥 𝐺
4		smfdivdmmbl2.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5		smfdivdmmbl2.5	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑉 )
6		smfdivdmmbl2.6	⊢ ( 𝜑 → 𝐺 ∈ ( SMblFn ‘ 𝑆 ) )
7		smfdivdmmbl2.7	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
8		smfdivdmmbl2.8	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )
9		smfdivdmmbl2.9	⊢ 𝐷 = { 𝑥 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 }
10		smfdivdmmbl2.10	⊢ 𝐻 = ( 𝑥 ∈ ( dom 𝐹 ∩ 𝐷 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
11	2	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
12		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 }
13	9 12	nfcxfr	⊢ Ⅎ 𝑥 𝐷
14	11 13	nfin	⊢ Ⅎ 𝑥 ( dom 𝐹 ∩ 𝐷 )
15		ovex	⊢ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ∈ V
16	14 15 10	dmmptif	⊢ dom 𝐻 = ( dom 𝐹 ∩ 𝐷 )
17	5	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
18	17 7	eqeltrd	⊢ ( 𝜑 → dom 𝐹 ∈ 𝑆 )
19	4 8	salrestss	⊢ ( 𝜑 → ( 𝑆 ↾t dom 𝐺 ) ⊆ 𝑆 )
20		eqid	⊢ dom 𝐺 = dom 𝐺
21	1 3 4 6 20	smfpimne2	⊢ ( 𝜑 → { 𝑥 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑥 ) ≠ 0 } ∈ ( 𝑆 ↾t dom 𝐺 ) )
22	9 21	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑆 ↾t dom 𝐺 ) )
23	19 22	sseldd	⊢ ( 𝜑 → 𝐷 ∈ 𝑆 )
24	4 18 23	salincld	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝐷 ) ∈ 𝑆 )
25	16 24	eqeltrid	⊢ ( 𝜑 → dom 𝐻 ∈ 𝑆 )