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	|- F/_ x F
	muldmmbl2.2	|- F/_ x G
	muldmmbl2.3	|- ( ph -> S e. SAlg )
	muldmmbl2.4	|- ( ph -> dom F e. S )
	muldmmbl2.5	|- ( ph -> dom G e. S )
	muldmmbl2.6	|- H = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) )
Assertion	muldmmbl2	|- ( ph -> dom H e. S )

Proof

Step	Hyp	Ref	Expression
1		muldmmbl2.1	|- F/_ x F
2		muldmmbl2.2	|- F/_ x G
3		muldmmbl2.3	|- ( ph -> S e. SAlg )
4		muldmmbl2.4	|- ( ph -> dom F e. S )
5		muldmmbl2.5	|- ( ph -> dom G e. S )
6		muldmmbl2.6	|- H = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) )
7	1	nfdm	|- F/_ x dom F
8	2	nfdm	|- F/_ x dom G
9	7 8	nfin	|- F/_ x ( dom F i^i dom G )
10		ovex	|- ( ( F ` x ) x. ( G ` x ) ) e. _V
11	9 10 6	dmmptif	|- dom H = ( dom F i^i dom G )
12	11	a1i	|- ( ph -> dom H = ( dom F i^i dom G ) )
13	3 4 5	salincld	|- ( ph -> ( dom F i^i dom G ) e. S )
14	12 13	eqeltrd	|- ( ph -> dom H e. S )