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	⊢ Ⅎ 𝑥 𝐹
	adddmmbl2.2	⊢ Ⅎ 𝑥 𝐺
	adddmmbl2.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	adddmmbl2.4	⊢ ( 𝜑 → dom 𝐹 ∈ 𝑆 )
	adddmmbl2.5	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )
	adddmmbl2.6	⊢ 𝐻 = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
Assertion	adddmmbl2	⊢ ( 𝜑 → dom 𝐻 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		adddmmbl2.1	⊢ Ⅎ 𝑥 𝐹
2		adddmmbl2.2	⊢ Ⅎ 𝑥 𝐺
3		adddmmbl2.3	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
4		adddmmbl2.4	⊢ ( 𝜑 → dom 𝐹 ∈ 𝑆 )
5		adddmmbl2.5	⊢ ( 𝜑 → dom 𝐺 ∈ 𝑆 )
6		adddmmbl2.6	⊢ 𝐻 = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
7	1	nfdm	⊢ Ⅎ 𝑥 dom 𝐹
8	2	nfdm	⊢ Ⅎ 𝑥 dom 𝐺
9	7 8	nfin	⊢ Ⅎ 𝑥 ( dom 𝐹 ∩ dom 𝐺 )
10		ovex	⊢ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ∈ V
11	9 10 6	dmmptif	⊢ dom 𝐻 = ( dom 𝐹 ∩ dom 𝐺 )
12	11	a1i	⊢ ( 𝜑 → dom 𝐻 = ( dom 𝐹 ∩ dom 𝐺 ) )
13	3 4 5	salincld	⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) ∈ 𝑆 )
14	12 13	eqeltrd	⊢ ( 𝜑 → dom 𝐻 ∈ 𝑆 )