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	⊢ Ⅎ 𝑥 𝜑
	smfdivdmmbl.2	⊢ Ⅎ 𝑥 𝐵
	smfdivdmmbl.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfdivdmmbl.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	smfdivdmmbl.5	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	smfdivdmmbl.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ 𝑊 )
	smfdivdmmbl.7	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfdivdmmbl.8	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ 𝐷 ≠ 0 }
Assertion	smfdivdmmbl	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐸 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		smfdivdmmbl.1	⊢ Ⅎ 𝑥 𝜑
2		smfdivdmmbl.2	⊢ Ⅎ 𝑥 𝐵
3		smfdivdmmbl.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		smfdivdmmbl.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
5		smfdivdmmbl.5	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
6		smfdivdmmbl.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ 𝑊 )
7		smfdivdmmbl.7	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
8		smfdivdmmbl.8	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ 𝐷 ≠ 0 }
9		nfcv	⊢ Ⅎ 𝑥 ℝ
10	1 2 3 6 7	smffmptf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) : 𝐵 ⟶ ℝ )
11	2 9 10	fvmptelcdmf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℝ )
12		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
13	1 2 3 5 11 7 12 8	smfdmmblpimne	⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
14	3 4 13	salincld	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐸 ) ∈ 𝑆 )