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

Proof

Step	Hyp	Ref	Expression
1		adddmmbl2.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		adddmmbl2.2	$$⊢\underset{\_}{Ⅎ}xG$$
3		adddmmbl2.3	$$⊢\phi \to S\in \mathrm{SAlg}$$
4		adddmmbl2.4	$$⊢\phi \to \mathrm{dom}F\in S$$
5		adddmmbl2.5	$$⊢\phi \to \mathrm{dom}G\in S$$
6		adddmmbl2.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$$