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	$⊢ Ⅎ x φ$
	smfmulc1.s	$⊢ φ \to S \in SAlg$
	smfmulc1.a	$⊢ φ \to A \in V$
	smfmulc1.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	smfmulc1.c	$⊢ φ \to C \in ℝ$
	smfmulc1.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
Assertion	smfmulc1	$⊢ φ \to (x \in A ⟼ C B) \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfmulc1.x	$⊢ Ⅎ x φ$
2		smfmulc1.s	$⊢ φ \to S \in SAlg$
3		smfmulc1.a	$⊢ φ \to A \in V$
4		smfmulc1.b	$⊢ (φ \land x \in A) \to B \in ℝ$
5		smfmulc1.c	$⊢ φ \to C \in ℝ$
6		smfmulc1.m	$⊢ φ \to (x \in A ⟼ B) \in SMblFn (S)$
7		inidm	$⊢ A \cap A = A$
8	7	eqcomi	$⊢ A = A \cap A$
9	8	mpteq1i	$⊢ (x \in A ⟼ C B) = (x \in (A \cap A) ⟼ C B)$
10	9	a1i	$⊢ φ \to (x \in A ⟼ C B) = (x \in (A \cap A) ⟼ C B)$
11	5	adantr	$⊢ (φ \land x \in A) \to C \in ℝ$
12		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
13	1 12 4	dmmptdf	$⊢ φ \to dom (x \in A ⟼ B) = A$
14	13	eqcomd	$⊢ φ \to A = dom (x \in A ⟼ B)$
15		eqid	$⊢ dom (x \in A ⟼ B) = dom (x \in A ⟼ B)$
16	2 6 15	smfdmss	$⊢ φ \to dom (x \in A ⟼ B) \subseteq ⋃ S$
17	14 16	eqsstrd	$⊢ φ \to A \subseteq ⋃ S$
18		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
19	1 2 17 5 18	smfconst	$⊢ φ \to (x \in A ⟼ C) \in SMblFn (S)$
20	1 2 3 11 4 19 6	smfmul	$⊢ φ \to (x \in (A \cap A) ⟼ C B) \in SMblFn (S)$
21	10 20	eqeltrd	$⊢ φ \to (x \in A ⟼ C B) \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfmulc1

Proof