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	|- F/ x ph
	muldmmbl.2	|- F/_ x A
	muldmmbl.3	|- F/_ x B
	muldmmbl.4	|- ( ph -> S e. SAlg )
	muldmmbl.5	|- ( ph -> A e. S )
	muldmmbl.6	|- ( ph -> B e. S )
Assertion	muldmmbl	|- ( ph -> dom ( x e. ( A i^i B ) |-> ( C x. D ) ) e. S )

Proof

Step	Hyp	Ref	Expression
1		muldmmbl.1	|- F/ x ph
2		muldmmbl.2	|- F/_ x A
3		muldmmbl.3	|- F/_ x B
4		muldmmbl.4	|- ( ph -> S e. SAlg )
5		muldmmbl.5	|- ( ph -> A e. S )
6		muldmmbl.6	|- ( ph -> B e. S )
7	2 3	nfin	|- F/_ x ( A i^i B )
8		eqid	|- ( x e. ( A i^i B ) |-> ( C x. D ) ) = ( x e. ( A i^i B ) |-> ( C x. D ) )
9		ovexd	|- ( ( ph /\ x e. ( A i^i B ) ) -> ( C x. D ) e. _V )
10	1 7 8 9	dmmptdff	|- ( ph -> dom ( x e. ( A i^i B ) |-> ( C x. D ) ) = ( A i^i B ) )
11	4 5 6	salincld	|- ( ph -> ( A i^i B ) e. S )
12	10 11	eqeltrd	|- ( ph -> dom ( x e. ( A i^i B ) |-> ( C x. D ) ) e. S )