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	$$⊢Ⅎx\phi$$
	muldmmbl.2	$$⊢\underset{\_}{Ⅎ}xA$$
	muldmmbl.3	$$⊢\underset{\_}{Ⅎ}xB$$
	muldmmbl.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
	muldmmbl.5	$$⊢\phi \to A\in S$$
	muldmmbl.6	$$⊢\phi \to B\in S$$
Assertion	muldmmbl	$$⊢\phi \to \mathrm{dom}\left(x\in \left(A\cap B\right)⟼CD\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		muldmmbl.1	$$⊢Ⅎx\phi$$
2		muldmmbl.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		muldmmbl.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		muldmmbl.4	$$⊢\phi \to S\in \mathrm{SAlg}$$
5		muldmmbl.5	$$⊢\phi \to A\in S$$
6		muldmmbl.6	$$⊢\phi \to B\in S$$
7	2 3	nfin	$$⊢\underset{\_}{Ⅎ}x\left(A\cap B\right)$$
8		eqid	$$⊢\left(x\in \left(A\cap B\right)⟼CD\right)=\left(x\in \left(A\cap B\right)⟼CD\right)$$
9		ovexd	$$⊢\left(\phi \wedge x\in \left(A\cap B\right)\right)\to CD\in \mathrm{V}$$
10	1 7 8 9	dmmptdff	$$⊢\phi \to \mathrm{dom}\left(x\in \left(A\cap B\right)⟼CD\right)=A\cap B$$
11	4 5 6	salincld	$$⊢\phi \to A\cap B\in S$$
12	10 11	eqeltrd	$$⊢\phi \to \mathrm{dom}\left(x\in \left(A\cap B\right)⟼CD\right)\in S$$