Theorem smfadd

Description: The sum of two sigma-measurable functions is measurable. Proposition 121E (b) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfadd.x	⊢ Ⅎ 𝑥 𝜑
	smfadd.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfadd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	smfadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	smfadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
	smfadd.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfadd.n	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
Assertion	smfadd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 + 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfadd.x	⊢ Ⅎ 𝑥 𝜑
2		smfadd.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfadd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		smfadd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
5		smfadd.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
6		smfadd.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
7		smfadd.n	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
8		nfv	⊢ Ⅎ 𝑎 𝜑
9		elinel1	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) → 𝑥 ∈ 𝐴 )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐴 )
11	1 10	ssdf	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴 )
12		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
13	1 12 4	dmmptdf	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
14	13	eqcomd	⊢ ( 𝜑 → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
15		eqid	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
16	2 6 15	smfdmss	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ∪ 𝑆 )
17	14 16	eqsstrd	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑆 )
18	11 17	sstrd	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ⊆ ∪ 𝑆 )
19	10 4	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ ℝ )
20		elinel2	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) → 𝑥 ∈ 𝐶 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐶 )
22	21 5	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐷 ∈ ℝ )
23	19 22	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐵 + 𝐷 ) ∈ ℝ )
24		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 + 𝐷 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 + 𝐷 ) )
25	1 23 24	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 + 𝐷 ) ) : ( 𝐴 ∩ 𝐶 ) ⟶ ℝ )
26	25	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐵 + 𝐷 ) ∈ ℝ )
27		nfv	⊢ Ⅎ 𝑥 𝑎 ∈ ℝ
28	1 27	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℝ )
29	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
30	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ 𝑉 )
31	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
32	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ∈ ℝ )
33	6	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
34	7	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) ∈ ( SMblFn ‘ 𝑆 ) )
35		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
36		oveq2	⊢ ( 𝑟 = 𝑞 → ( 𝑝 + 𝑟 ) = ( 𝑝 + 𝑞 ) )
37	36	breq1d	⊢ ( 𝑟 = 𝑞 → ( ( 𝑝 + 𝑟 ) < 𝑎 ↔ ( 𝑝 + 𝑞 ) < 𝑎 ) )
38	37	cbvrabv	⊢ { 𝑟 ∈ ℚ ∣ ( 𝑝 + 𝑟 ) < 𝑎 } = { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑎 }
39	38	mpteq2i	⊢ ( 𝑝 ∈ ℚ ↦ { 𝑟 ∈ ℚ ∣ ( 𝑝 + 𝑟 ) < 𝑎 } ) = ( 𝑝 ∈ ℚ ↦ { 𝑞 ∈ ℚ ∣ ( 𝑝 + 𝑞 ) < 𝑎 } )
40	28 29 30 31 32 33 34 35 39	smfaddlem2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∣ ( 𝐵 + 𝐷 ) < 𝑎 } ∈ ( 𝑆 ↾t ( 𝐴 ∩ 𝐶 ) ) )
41	1 8 2 18 26 40	issmfdmpt	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↦ ( 𝐵 + 𝐷 ) ) ∈ ( SMblFn ‘ 𝑆 ) )