Theorem adddmmbl

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	adddmmbl.1	⊢ Ⅎ 𝑥 𝜑
	adddmmbl.2	⊢ Ⅎ 𝑥 𝐴
	adddmmbl.3	⊢ Ⅎ 𝑥 𝐵
	adddmmbl.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	adddmmbl.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	adddmmbl.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
Assertion	adddmmbl	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 + 𝐷 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		adddmmbl.1	⊢ Ⅎ 𝑥 𝜑
2		adddmmbl.2	⊢ Ⅎ 𝑥 𝐴
3		adddmmbl.3	⊢ Ⅎ 𝑥 𝐵
4		adddmmbl.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5		adddmmbl.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
6		adddmmbl.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
7	2 3	nfin	⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐵 )
8		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 + 𝐷 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 + 𝐷 ) )
9		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐶 + 𝐷 ) ∈ V )
10	1 7 8 9	dmmptdff	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 + 𝐷 ) ) = ( 𝐴 ∩ 𝐵 ) )
11	4 5 6	salincld	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 )
12	10 11	eqeltrd	⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↦ ( 𝐶 + 𝐷 ) ) ∈ 𝑆 )