Metamath Proof Explorer

Theorem mbfres2cn

Description: Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A , then F is measurable on the whole domain. Similar to mbfres2 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mbfres2cn.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
mbfres2cn.b ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ MblFn )
mbfres2cn.c ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ MblFn )
mbfres2cn.a ⊢ ( 𝜑 → ( 𝐵 ∪ 𝐶 ) = 𝐴 )
Assertion mbfres2cn ( 𝜑 → 𝐹 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfres2cn.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 mbfres2cn.b ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ MblFn )
3 mbfres2cn.c ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ MblFn )
4 mbfres2cn.a ⊢ ( 𝜑 → ( 𝐵 ∪ 𝐶 ) = 𝐴 )
5 ref ⊢ ℜ : ℂ ⟶ ℝ
6 fco ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ℜ ∘ 𝐹 ) : 𝐴 ⟶ ℝ )
7 5 1 6 sylancr ⊢ ( 𝜑 → ( ℜ ∘ 𝐹 ) : 𝐴 ⟶ ℝ )
8 resco ⊢ ( ( ℜ ∘ 𝐹 ) ↾ 𝐵 ) = ( ℜ ∘ ( 𝐹 ↾ 𝐵 ) )
9 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
10 ismbfcn ⊢ ( ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ → ( ( 𝐹 ↾ 𝐵 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn ) ) )
11 1 9 10 3syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn ) ) )
12 2 11 mpbid ⊢ ( 𝜑 → ( ( ℜ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn ) )
13 12 simpld ⊢ ( 𝜑 → ( ℜ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn )
14 8 13 eqeltrid ⊢ ( 𝜑 → ( ( ℜ ∘ 𝐹 ) ↾ 𝐵 ) ∈ MblFn )
15 resco ⊢ ( ( ℜ ∘ 𝐹 ) ↾ 𝐶 ) = ( ℜ ∘ ( 𝐹 ↾ 𝐶 ) )
16 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ 𝐶 ) : ( 𝐴 ∩ 𝐶 ) ⟶ ℂ )
17 ismbfcn ⊢ ( ( 𝐹 ↾ 𝐶 ) : ( 𝐴 ∩ 𝐶 ) ⟶ ℂ → ( ( 𝐹 ↾ 𝐶 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn ) ) )
18 1 16 17 3syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn ) ) )
19 3 18 mpbid ⊢ ( 𝜑 → ( ( ℜ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn ) )
20 19 simpld ⊢ ( 𝜑 → ( ℜ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn )
21 15 20 eqeltrid ⊢ ( 𝜑 → ( ( ℜ ∘ 𝐹 ) ↾ 𝐶 ) ∈ MblFn )
22 7 14 21 4 mbfres2 ⊢ ( 𝜑 → ( ℜ ∘ 𝐹 ) ∈ MblFn )
23 imf ⊢ ℑ : ℂ ⟶ ℝ
24 fco ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ℑ ∘ 𝐹 ) : 𝐴 ⟶ ℝ )
25 23 1 24 sylancr ⊢ ( 𝜑 → ( ℑ ∘ 𝐹 ) : 𝐴 ⟶ ℝ )
26 resco ⊢ ( ( ℑ ∘ 𝐹 ) ↾ 𝐵 ) = ( ℑ ∘ ( 𝐹 ↾ 𝐵 ) )
27 12 simprd ⊢ ( 𝜑 → ( ℑ ∘ ( 𝐹 ↾ 𝐵 ) ) ∈ MblFn )
28 26 27 eqeltrid ⊢ ( 𝜑 → ( ( ℑ ∘ 𝐹 ) ↾ 𝐵 ) ∈ MblFn )
29 resco ⊢ ( ( ℑ ∘ 𝐹 ) ↾ 𝐶 ) = ( ℑ ∘ ( 𝐹 ↾ 𝐶 ) )
30 19 simprd ⊢ ( 𝜑 → ( ℑ ∘ ( 𝐹 ↾ 𝐶 ) ) ∈ MblFn )
31 29 30 eqeltrid ⊢ ( 𝜑 → ( ( ℑ ∘ 𝐹 ) ↾ 𝐶 ) ∈ MblFn )
32 25 28 31 4 mbfres2 ⊢ ( 𝜑 → ( ℑ ∘ 𝐹 ) ∈ MblFn )
33 ismbfcn ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )
34 1 33 syl ⊢ ( 𝜑 → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )
35 22 32 34 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ MblFn )