Theorem adddmmbl2

Description: If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first 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 addition. (Contributed by Glauco Siliprandi, 30-Dec-2024)

	Ref	Expression
Hypotheses	adddmmbl2.1	|- F/_ x F
	adddmmbl2.2	|- F/_ x G
	adddmmbl2.3	|- ( ph -> S e. SAlg )
	adddmmbl2.4	|- ( ph -> dom F e. S )
	adddmmbl2.5	|- ( ph -> dom G e. S )
	adddmmbl2.6	|- H = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) + ( G ` x ) ) )
Assertion	adddmmbl2	|- ( ph -> dom H e. S )

Proof

Step	Hyp	Ref	Expression
1		adddmmbl2.1	|- F/_ x F
2		adddmmbl2.2	|- F/_ x G
3		adddmmbl2.3	|- ( ph -> S e. SAlg )
4		adddmmbl2.4	|- ( ph -> dom F e. S )
5		adddmmbl2.5	|- ( ph -> dom G e. S )
6		adddmmbl2.6	|- H = ( x e. ( dom F i^i dom G ) |-> ( ( F ` 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 ) + ( 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 )