Theorem smfmulc1

Description: A sigma-measurable function multiplied by a constant is sigma-measurable. Proposition 121E (c) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfmulc1.x	⊢ Ⅎ 𝑥 𝜑
	smfmulc1.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfmulc1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	smfmulc1.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	smfmulc1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	smfmulc1.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
Assertion	smfmulc1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfmulc1.x	⊢ Ⅎ 𝑥 𝜑
2		smfmulc1.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfmulc1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		smfmulc1.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
5		smfmulc1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6		smfmulc1.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
7		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
8	7	eqcomi	⊢ 𝐴 = ( 𝐴 ∩ 𝐴 )
9	8	mpteq1i	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) ↦ ( 𝐶 · 𝐵 ) )
10	9	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) ↦ ( 𝐶 · 𝐵 ) ) )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
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		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
19	1 2 17 5 18	smfconst	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ( SMblFn ‘ 𝑆 ) )
20	1 2 3 11 4 19 6	smfmul	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐴 ) ↦ ( 𝐶 · 𝐵 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
21	10 20	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ ( SMblFn ‘ 𝑆 ) )