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	$$⊢\underset{\_}{Ⅎ}xF$$
	muldmmbl2.2	$$⊢\underset{\_}{Ⅎ}xG$$
	muldmmbl2.3	$$⊢\phi \to S\in \mathrm{SAlg}$$
	muldmmbl2.4	$$⊢\phi \to \mathrm{dom}F\in S$$
	muldmmbl2.5	$$⊢\phi \to \mathrm{dom}G\in S$$
	muldmmbl2.6	$$⊢H=\left(x\in \left(\mathrm{dom}F\cap \mathrm{dom}G\right)⟼F\left(x\right)G\left(x\right)\right)$$
Assertion	muldmmbl2	$$⊢\phi \to \mathrm{dom}H\in S$$

Proof

Step	Hyp	Ref	Expression
1		muldmmbl2.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		muldmmbl2.2	$$⊢\underset{\_}{Ⅎ}xG$$
3		muldmmbl2.3	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		muldmmbl2.4	$$⊢\phi \to \mathrm{dom}F\in S$$
5		muldmmbl2.5	$$⊢\phi \to \mathrm{dom}G\in S$$
6		muldmmbl2.6	$$⊢H=\left(x\in \left(\mathrm{dom}F\cap \mathrm{dom}G\right)⟼F\left(x\right)G\left(x\right)\right)$$
7	1	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}F$$
8	2	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}G$$
9	7 8	nfin	$$⊢\underset{\_}{Ⅎ}x\left(\mathrm{dom}F\cap \mathrm{dom}G\right)$$
10		ovex	$$⊢F\left(x\right)G\left(x\right)\in \mathrm{V}$$
11	9 10 6	dmmptif	$$⊢\mathrm{dom}H=\mathrm{dom}F\cap \mathrm{dom}G$$
12	11	a1i	$$⊢\phi \to \mathrm{dom}H=\mathrm{dom}F\cap \mathrm{dom}G$$
13	3 4 5	salincld	$$⊢\phi \to \mathrm{dom}F\cap \mathrm{dom}G\in S$$
14	12 13	eqeltrd	$$⊢\phi \to \mathrm{dom}H\in S$$