Theorem muldmmbl2

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	muldmmbl2.1	⊢ Ⅎ 𝑥 𝐹
	muldmmbl2.2	⊢ Ⅎ 𝑥 𝐺
	muldmmbl2.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	muldmmbl2.4	⊢ ( 𝜑 → dom 𝐹 ∈ 𝑆 )
	muldmmbl2.5	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )
	muldmmbl2.6	⊢ 𝐻 = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
Assertion	muldmmbl2	⊢ ( 𝜑 → dom 𝐻 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		muldmmbl2.1	⊢ Ⅎ 𝑥 𝐹
2		muldmmbl2.2	⊢ Ⅎ 𝑥 𝐺
3		muldmmbl2.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		muldmmbl2.4	⊢ ( 𝜑 → dom 𝐹 ∈ 𝑆 )
5		muldmmbl2.5	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )
6		muldmmbl2.6	⊢ 𝐻 = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
7	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
8	2	nfdm	⊢ Ⅎ 𝑥 dom 𝐺
9	7 8	nfin	⊢ Ⅎ 𝑥 ( dom 𝐹 ∩ dom 𝐺 )
10		ovex	⊢ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ V
11	9 10 6	dmmptif	⊢ dom 𝐻 = ( dom 𝐹 ∩ dom 𝐺 )
12	11	a1i	⊢ ( 𝜑 → dom 𝐻 = ( dom 𝐹 ∩ dom 𝐺 ) )
13	3 4 5	salincld	⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) ∈ 𝑆 )
14	12 13	eqeltrd	⊢ ( 𝜑 → dom 𝐻 ∈ 𝑆 )