Theorem muldmmbl

Description: If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of Fremlin1, p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024)

	Ref	Expression
Hypotheses	muldmmbl.1	⊢ Ⅎ 𝑥 𝜑
	muldmmbl.2	⊢ Ⅎ 𝑥 𝐴
	muldmmbl.3	⊢ Ⅎ 𝑥 𝐵
	muldmmbl.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	muldmmbl.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	muldmmbl.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
Assertion	muldmmbl	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 · 𝐷 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		muldmmbl.1	⊢ Ⅎ 𝑥 𝜑
2		muldmmbl.2	⊢ Ⅎ 𝑥 𝐴
3		muldmmbl.3	⊢ Ⅎ 𝑥 𝐵
4		muldmmbl.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5		muldmmbl.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
6		muldmmbl.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
7	2 3	nfin	⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )
8		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 · 𝐷 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 · 𝐷 ) )
9		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐶 · 𝐷 ) ∈ V )
10	1 7 8 9	dmmptdff	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 · 𝐷 ) ) = ( 𝐴 ∩ 𝐵 ) )
11	4 5 6	salincld	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )
12	10 11	eqeltrd	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 · 𝐷 ) ) ∈ 𝑆 )