mbfmulc2

Description: A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	mbfmulc2.1	$⊢ φ \to C \in ℂ$
	mbfmulc2.2	$⊢ (φ \land x \in A) \to B \in V$
	mbfmulc2.3	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
Assertion	mbfmulc2	$⊢ φ \to (x \in A ⟼ C B) \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmulc2.1	$⊢ φ \to C \in ℂ$
2		mbfmulc2.2	$⊢ (φ \land x \in A) \to B \in V$
3		mbfmulc2.3	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
4	3 2	mbfdm2	$⊢ φ \to A \in dom vol$
5	1	recld	$⊢ φ \to ℜ (C) \in ℝ$
6	5	adantr	$⊢ (φ \land x \in A) \to ℜ (C) \in ℝ$
7	6	recnd	$⊢ (φ \land x \in A) \to ℜ (C) \in ℂ$
8	3 2	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
9	8	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
10	9	recnd	$⊢ (φ \land x \in A) \to ℜ (B) \in ℂ$
11	7 10	mulcld	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) \in ℂ$
12		ovexd	$⊢ (φ \land x \in A) \to (- ℑ (C)) ℑ (B) \in V$
13		fconstmpt	$⊢ A \times \{ℜ (C)\} = (x \in A ⟼ ℜ (C))$
14	13	a1i	$⊢ φ \to A \times \{ℜ (C)\} = (x \in A ⟼ ℜ (C))$
15		eqidd	$⊢ φ \to (x \in A ⟼ ℜ (B)) = (x \in A ⟼ ℜ (B))$
16	4 6 9 14 15	offval2	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) = (x \in A ⟼ ℜ (C) ℜ (B))$
17	1	imcld	$⊢ φ \to ℑ (C) \in ℝ$
18	17	renegcld	$⊢ φ \to - ℑ (C) \in ℝ$
19	18	adantr	$⊢ (φ \land x \in A) \to - ℑ (C) \in ℝ$
20	8	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
21		fconstmpt	$⊢ A \times \{- ℑ (C)\} = (x \in A ⟼ - ℑ (C))$
22	21	a1i	$⊢ φ \to A \times \{- ℑ (C)\} = (x \in A ⟼ - ℑ (C))$
23		eqidd	$⊢ φ \to (x \in A ⟼ ℑ (B)) = (x \in A ⟼ ℑ (B))$
24	4 19 20 22 23	offval2	$⊢ φ \to (A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) = (x \in A ⟼ (- ℑ (C)) ℑ (B))$
25	4 11 12 16 24	offval2	$⊢ φ \to ((A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B))) +_{f} ((A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B))) = (x \in A ⟼ ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B))$
26	17	adantr	$⊢ (φ \land x \in A) \to ℑ (C) \in ℝ$
27	26	recnd	$⊢ (φ \land x \in A) \to ℑ (C) \in ℂ$
28	20	recnd	$⊢ (φ \land x \in A) \to ℑ (B) \in ℂ$
29	27 28	mulcld	$⊢ (φ \land x \in A) \to ℑ (C) ℑ (B) \in ℂ$
30	11 29	negsubd	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) + (- ℑ (C) ℑ (B)) = ℜ (C) ℜ (B) - ℑ (C) ℑ (B)$
31	27 28	mulneg1d	$⊢ (φ \land x \in A) \to (- ℑ (C)) ℑ (B) = - ℑ (C) ℑ (B)$
32	31	oveq2d	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B) = ℜ (C) ℜ (B) + (- ℑ (C) ℑ (B))$
33	1	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
34	33 8	remuld	$⊢ (φ \land x \in A) \to ℜ (C B) = ℜ (C) ℜ (B) - ℑ (C) ℑ (B)$
35	30 32 34	3eqtr4d	$⊢ (φ \land x \in A) \to ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B) = ℜ (C B)$
36	35	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℜ (C) ℜ (B) + (- ℑ (C)) ℑ (B)) = (x \in A ⟼ ℜ (C B))$
37	25 36	eqtrd	$⊢ φ \to ((A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B))) +_{f} ((A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B))) = (x \in A ⟼ ℜ (C B))$
38	8	ismbfcn2	$⊢ φ \to ((x \in A ⟼ B) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn))$
39	3 38	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn)$
40	39	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in MblFn$
41	10	fmpttd	$⊢ φ \to (x \in A ⟼ ℜ (B)) : A ⟶ ℂ$
42	40 5 41	mbfmulc2re	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) \in MblFn$
43	39	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in MblFn$
44	28	fmpttd	$⊢ φ \to (x \in A ⟼ ℑ (B)) : A ⟶ ℂ$
45	43 18 44	mbfmulc2re	$⊢ φ \to (A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) \in MblFn$
46	42 45	mbfadd	$⊢ φ \to ((A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℜ (B))) +_{f} ((A \times \{- ℑ (C)\}) \times_{f} (x \in A ⟼ ℑ (B))) \in MblFn$
47	37 46	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℜ (C B)) \in MblFn$
48		ovexd	$⊢ (φ \land x \in A) \to ℜ (C) ℑ (B) \in V$
49		ovexd	$⊢ (φ \land x \in A) \to ℑ (C) ℜ (B) \in V$
50	4 6 20 14 23	offval2	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) = (x \in A ⟼ ℜ (C) ℑ (B))$
51		fconstmpt	$⊢ A \times \{ℑ (C)\} = (x \in A ⟼ ℑ (C))$
52	51	a1i	$⊢ φ \to A \times \{ℑ (C)\} = (x \in A ⟼ ℑ (C))$
53	4 26 9 52 15	offval2	$⊢ φ \to (A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) = (x \in A ⟼ ℑ (C) ℜ (B))$
54	4 48 49 50 53	offval2	$⊢ φ \to ((A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B))) +_{f} ((A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B))) = (x \in A ⟼ ℜ (C) ℑ (B) + ℑ (C) ℜ (B))$
55	33 8	immuld	$⊢ (φ \land x \in A) \to ℑ (C B) = ℜ (C) ℑ (B) + ℑ (C) ℜ (B)$
56	55	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℑ (C B)) = (x \in A ⟼ ℜ (C) ℑ (B) + ℑ (C) ℜ (B))$
57	54 56	eqtr4d	$⊢ φ \to ((A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B))) +_{f} ((A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B))) = (x \in A ⟼ ℑ (C B))$
58	43 5 44	mbfmulc2re	$⊢ φ \to (A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B)) \in MblFn$
59	40 17 41	mbfmulc2re	$⊢ φ \to (A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B)) \in MblFn$
60	58 59	mbfadd	$⊢ φ \to ((A \times \{ℜ (C)\}) \times_{f} (x \in A ⟼ ℑ (B))) +_{f} ((A \times \{ℑ (C)\}) \times_{f} (x \in A ⟼ ℜ (B))) \in MblFn$
61	57 60	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℑ (C B)) \in MblFn$
62	33 8	mulcld	$⊢ (φ \land x \in A) \to C B \in ℂ$
63	62	ismbfcn2	$⊢ φ \to ((x \in A ⟼ C B) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (C B)) \in MblFn \land (x \in A ⟼ ℑ (C B)) \in MblFn))$
64	47 61 63	mpbir2and	$⊢ φ \to (x \in A ⟼ C B) \in MblFn$

Metamath Proof Explorer

Theorem mbfmulc2

Proof