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	|- F/ x ph
	smfmulc1.s	|- ( ph -> S e. SAlg )
	smfmulc1.a	|- ( ph -> A e. V )
	smfmulc1.b	|- ( ( ph /\ x e. A ) -> B e. RR )
	smfmulc1.c	|- ( ph -> C e. RR )
	smfmulc1.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
Assertion	smfmulc1	|- ( ph -> ( x e. A |-> ( C x. B ) ) e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		smfmulc1.x	|- F/ x ph
2		smfmulc1.s	|- ( ph -> S e. SAlg )
3		smfmulc1.a	|- ( ph -> A e. V )
4		smfmulc1.b	|- ( ( ph /\ x e. A ) -> B e. RR )
5		smfmulc1.c	|- ( ph -> C e. RR )
6		smfmulc1.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
7		inidm	|- ( A i^i A ) = A
8	7	eqcomi	|- A = ( A i^i A )
9	8	mpteq1i	|- ( x e. A |-> ( C x. B ) ) = ( x e. ( A i^i A ) |-> ( C x. B ) )
10	9	a1i	|- ( ph -> ( x e. A |-> ( C x. B ) ) = ( x e. ( A i^i A ) |-> ( C x. B ) ) )
11	5	adantr	|- ( ( ph /\ x e. A ) -> C e. RR )
12		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
13	1 12 4	dmmptdf	|- ( ph -> dom ( x e. A |-> B ) = A )
14	13	eqcomd	|- ( ph -> A = dom ( x e. A |-> B ) )
15		eqid	|- dom ( x e. A |-> B ) = dom ( x e. A |-> B )
16	2 6 15	smfdmss	|- ( ph -> dom ( x e. A |-> B ) C_ U. S )
17	14 16	eqsstrd	|- ( ph -> A C_ U. S )
18		eqid	|- ( x e. A |-> C ) = ( x e. A |-> C )
19	1 2 17 5 18	smfconst	|- ( ph -> ( x e. A |-> C ) e. ( SMblFn ` S ) )
20	1 2 3 11 4 19 6	smfmul	|- ( ph -> ( x e. ( A i^i A ) |-> ( C x. B ) ) e. ( SMblFn ` S ) )
21	10 20	eqeltrd	|- ( ph -> ( x e. A |-> ( C x. B ) ) e. ( SMblFn ` S ) )