mbfmulc2re

Description: Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014)

	Ref	Expression
Hypotheses	mbfmulc2re.1	$⊢ φ \to F \in MblFn$
	mbfmulc2re.2	$⊢ φ \to B \in ℝ$
	mbfmulc2re.3	$⊢ φ \to F : A ⟶ ℂ$
Assertion	mbfmulc2re	$⊢ φ \to (A \times \{B\}) \times_{f} F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmulc2re.1	$⊢ φ \to F \in MblFn$
2		mbfmulc2re.2	$⊢ φ \to B \in ℝ$
3		mbfmulc2re.3	$⊢ φ \to F : A ⟶ ℂ$
4	3	fdmd	$⊢ φ \to dom F = A$
5	1	dmexd	$⊢ φ \to dom F \in V$
6	4 5	eqeltrrd	$⊢ φ \to A \in V$
7	2	adantr	$⊢ (φ \land x \in A) \to B \in ℝ$
8	3	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in ℂ$
9		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
10	9	a1i	$⊢ φ \to A \times \{B\} = (x \in A ⟼ B)$
11	3	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
12	6 7 8 10 11	offval2	$⊢ φ \to (A \times \{B\}) \times_{f} F = (x \in A ⟼ B F (x))$
13	7 8	remul2d	$⊢ (φ \land x \in A) \to ℜ (B F (x)) = B ℜ (F (x))$
14	13	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℜ (B F (x))) = (x \in A ⟼ B ℜ (F (x)))$
15	8	recld	$⊢ (φ \land x \in A) \to ℜ (F (x)) \in ℝ$
16		eqidd	$⊢ φ \to (x \in A ⟼ ℜ (F (x))) = (x \in A ⟼ ℜ (F (x)))$
17	6 7 15 10 16	offval2	$⊢ φ \to (A \times \{B\}) \times_{f} (x \in A ⟼ ℜ (F (x))) = (x \in A ⟼ B ℜ (F (x)))$
18	14 17	eqtr4d	$⊢ φ \to (x \in A ⟼ ℜ (B F (x))) = (A \times \{B\}) \times_{f} (x \in A ⟼ ℜ (F (x)))$
19	11 1	eqeltrrd	$⊢ φ \to (x \in A ⟼ F (x)) \in MblFn$
20	8	ismbfcn2	$⊢ φ \to ((x \in A ⟼ F (x)) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (F (x))) \in MblFn \land (x \in A ⟼ ℑ (F (x))) \in MblFn))$
21	19 20	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (F (x))) \in MblFn \land (x \in A ⟼ ℑ (F (x))) \in MblFn)$
22	21	simpld	$⊢ φ \to (x \in A ⟼ ℜ (F (x))) \in MblFn$
23	15	fmpttd	$⊢ φ \to (x \in A ⟼ ℜ (F (x))) : A ⟶ ℝ$
24	22 2 23	mbfmulc2lem	$⊢ φ \to (A \times \{B\}) \times_{f} (x \in A ⟼ ℜ (F (x))) \in MblFn$
25	18 24	eqeltrd	$⊢ φ \to (x \in A ⟼ ℜ (B F (x))) \in MblFn$
26	7 8	immul2d	$⊢ (φ \land x \in A) \to ℑ (B F (x)) = B ℑ (F (x))$
27	26	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℑ (B F (x))) = (x \in A ⟼ B ℑ (F (x)))$
28	8	imcld	$⊢ (φ \land x \in A) \to ℑ (F (x)) \in ℝ$
29		eqidd	$⊢ φ \to (x \in A ⟼ ℑ (F (x))) = (x \in A ⟼ ℑ (F (x)))$
30	6 7 28 10 29	offval2	$⊢ φ \to (A \times \{B\}) \times_{f} (x \in A ⟼ ℑ (F (x))) = (x \in A ⟼ B ℑ (F (x)))$
31	27 30	eqtr4d	$⊢ φ \to (x \in A ⟼ ℑ (B F (x))) = (A \times \{B\}) \times_{f} (x \in A ⟼ ℑ (F (x)))$
32	21	simprd	$⊢ φ \to (x \in A ⟼ ℑ (F (x))) \in MblFn$
33	28	fmpttd	$⊢ φ \to (x \in A ⟼ ℑ (F (x))) : A ⟶ ℝ$
34	32 2 33	mbfmulc2lem	$⊢ φ \to (A \times \{B\}) \times_{f} (x \in A ⟼ ℑ (F (x))) \in MblFn$
35	31 34	eqeltrd	$⊢ φ \to (x \in A ⟼ ℑ (B F (x))) \in MblFn$
36	2	recnd	$⊢ φ \to B \in ℂ$
37	36	adantr	$⊢ (φ \land x \in A) \to B \in ℂ$
38	37 8	mulcld	$⊢ (φ \land x \in A) \to B F (x) \in ℂ$
39	38	ismbfcn2	$⊢ φ \to ((x \in A ⟼ B F (x)) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (B F (x))) \in MblFn \land (x \in A ⟼ ℑ (B F (x))) \in MblFn))$
40	25 35 39	mpbir2and	$⊢ φ \to (x \in A ⟼ B F (x)) \in MblFn$
41	12 40	eqeltrd	$⊢ φ \to (A \times \{B\}) \times_{f} F \in MblFn$

Metamath Proof Explorer

Theorem mbfmulc2re

Proof