Theorem mbfmulc2

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

	Ref	Expression
Hypotheses	mbfmulc2.1	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	mbfmulc2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	mbfmulc2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
Assertion	mbfmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		mbfmulc2.1	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		mbfmulc2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		mbfmulc2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
4	3 2	mbfdm2	⊢ ( 𝜑 → 𝐴 ∈ dom vol )
5	1	recld	⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℝ )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
7	6	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
8	3 2	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
9	8	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
10	9	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
11	7 10	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
12		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ V )
13		fconstmpt	⊢ ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) )
14	13	a1i	⊢ ( 𝜑 → ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) )
15		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) )
16	4 6 9 14 15	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
17	1	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℝ )
18	17	renegcld	⊢ ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
20	8	imcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
21		fconstmpt	⊢ ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) )
22	21	a1i	⊢ ( 𝜑 → ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) ) )
23		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) )
24	4 19 20 22 23	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
25	4 11 12 16 24	offval2	⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
26	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
27	26	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
28	20	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
29	27 28	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
30	11 29	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
31	27 28	mulneg1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) = - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) )
32	31	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
33	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
34	33 8	remuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
35	30 32 34	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ℜ ‘ ( 𝐶 · 𝐵 ) ) )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) )
37	25 36	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) )
38	8	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
39	3 38	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) )
40	39	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
41	10	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
42	40 5 41	mbfmulc2re	⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
43	39	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
44	28	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
45	43 18 44	mbfmulc2re	⊢ ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
46	42 45	mbfadd	⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ) ∈ MblFn )
47	37 46	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
48		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ V )
49		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ V )
50	4 6 20 14 23	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
51		fconstmpt	⊢ ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) )
52	51	a1i	⊢ ( 𝜑 → ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) )
53	4 26 9 52 15	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
54	4 48 49 50 53	offval2	⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
55	33 8	immuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
56	55	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
57	54 56	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) )
58	43 5 44	mbfmulc2re	⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
59	40 17 41	mbfmulc2re	⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
60	58 59	mbfadd	⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ) ∈ MblFn )
61	57 60	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
62	33 8	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
63	62	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) ) )
64	47 61 63	mpbir2and	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )