This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
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 )