Theorem mbfmulc2re

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

	Ref	Expression
Hypotheses	mbfmulc2re.1	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
	mbfmulc2re.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	mbfmulc2re.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
Assertion	mbfmulc2re	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		mbfmulc2re.1	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2		mbfmulc2re.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		mbfmulc2re.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
4	3	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
5	1	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
6	4 5	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ V )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
8	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
9		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10	9	a1i	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
11	3	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
12	6 7 8 10 11	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) )
13	7 8	remul2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐵 · ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
14	13	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
15	8	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
16		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
17	6 7 15 10 16	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
18	14 17	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
19	11 1	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
20	8	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) ) )
21	19 20	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) )
22	21	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
23	15	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) : 𝐴 ⟶ ℝ )
24	22 2 23	mbfmulc2lem	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ MblFn )
25	18 24	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ MblFn )
26	7 8	immul2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐵 · ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
27	26	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
28	8	imcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
29		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
30	6 7 28 10 29	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
31	27 30	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
32	21	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
33	28	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) : 𝐴 ⟶ ℝ )
34	32 2 33	mbfmulc2lem	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ MblFn )
35	31 34	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ MblFn )
36	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
38	37 8	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
39	38	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ MblFn ) ) )
40	25 35 39	mpbir2and	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
41	12 40	eqeltrd	⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )