Metamath Proof Explorer


Theorem mbfres2

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. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfres2.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
mbfres2.2 ( 𝜑 → ( 𝐹𝐵 ) ∈ MblFn )
mbfres2.3 ( 𝜑 → ( 𝐹𝐶 ) ∈ MblFn )
mbfres2.4 ( 𝜑 → ( 𝐵𝐶 ) = 𝐴 )
Assertion mbfres2 ( 𝜑𝐹 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfres2.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
2 mbfres2.2 ( 𝜑 → ( 𝐹𝐵 ) ∈ MblFn )
3 mbfres2.3 ( 𝜑 → ( 𝐹𝐶 ) ∈ MblFn )
4 mbfres2.4 ( 𝜑 → ( 𝐵𝐶 ) = 𝐴 )
5 4 reseq2d ( 𝜑 → ( 𝐹 ↾ ( 𝐵𝐶 ) ) = ( 𝐹𝐴 ) )
6 ffn ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 Fn 𝐴 )
7 fnresdm ( 𝐹 Fn 𝐴 → ( 𝐹𝐴 ) = 𝐹 )
8 1 6 7 3syl ( 𝜑 → ( 𝐹𝐴 ) = 𝐹 )
9 5 8 eqtr2d ( 𝜑𝐹 = ( 𝐹 ↾ ( 𝐵𝐶 ) ) )
10 9 adantr ( ( 𝜑𝑥 ∈ ran (,) ) → 𝐹 = ( 𝐹 ↾ ( 𝐵𝐶 ) ) )
11 resundi ( 𝐹 ↾ ( 𝐵𝐶 ) ) = ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) )
12 10 11 eqtrdi ( ( 𝜑𝑥 ∈ ran (,) ) → 𝐹 = ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) ) )
13 12 cnveqd ( ( 𝜑𝑥 ∈ ran (,) ) → 𝐹 = ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) ) )
14 cnvun ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) ) = ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) )
15 13 14 eqtrdi ( ( 𝜑𝑥 ∈ ran (,) ) → 𝐹 = ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) ) )
16 15 imaeq1d ( ( 𝜑𝑥 ∈ ran (,) ) → ( 𝐹𝑥 ) = ( ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) ) “ 𝑥 ) )
17 imaundir ( ( ( 𝐹𝐵 ) ∪ ( 𝐹𝐶 ) ) “ 𝑥 ) = ( ( ( 𝐹𝐵 ) “ 𝑥 ) ∪ ( ( 𝐹𝐶 ) “ 𝑥 ) )
18 16 17 eqtrdi ( ( 𝜑𝑥 ∈ ran (,) ) → ( 𝐹𝑥 ) = ( ( ( 𝐹𝐵 ) “ 𝑥 ) ∪ ( ( 𝐹𝐶 ) “ 𝑥 ) ) )
19 ssun1 𝐵 ⊆ ( 𝐵𝐶 )
20 19 4 sseqtrid ( 𝜑𝐵𝐴 )
21 1 20 fssresd ( 𝜑 → ( 𝐹𝐵 ) : 𝐵 ⟶ ℝ )
22 ismbf ( ( 𝐹𝐵 ) : 𝐵 ⟶ ℝ → ( ( 𝐹𝐵 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ( 𝐹𝐵 ) “ 𝑥 ) ∈ dom vol ) )
23 21 22 syl ( 𝜑 → ( ( 𝐹𝐵 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ( 𝐹𝐵 ) “ 𝑥 ) ∈ dom vol ) )
24 2 23 mpbid ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ( 𝐹𝐵 ) “ 𝑥 ) ∈ dom vol )
25 24 r19.21bi ( ( 𝜑𝑥 ∈ ran (,) ) → ( ( 𝐹𝐵 ) “ 𝑥 ) ∈ dom vol )
26 ssun2 𝐶 ⊆ ( 𝐵𝐶 )
27 26 4 sseqtrid ( 𝜑𝐶𝐴 )
28 1 27 fssresd ( 𝜑 → ( 𝐹𝐶 ) : 𝐶 ⟶ ℝ )
29 ismbf ( ( 𝐹𝐶 ) : 𝐶 ⟶ ℝ → ( ( 𝐹𝐶 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ( 𝐹𝐶 ) “ 𝑥 ) ∈ dom vol ) )
30 28 29 syl ( 𝜑 → ( ( 𝐹𝐶 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ( 𝐹𝐶 ) “ 𝑥 ) ∈ dom vol ) )
31 3 30 mpbid ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ( 𝐹𝐶 ) “ 𝑥 ) ∈ dom vol )
32 31 r19.21bi ( ( 𝜑𝑥 ∈ ran (,) ) → ( ( 𝐹𝐶 ) “ 𝑥 ) ∈ dom vol )
33 unmbl ( ( ( ( 𝐹𝐵 ) “ 𝑥 ) ∈ dom vol ∧ ( ( 𝐹𝐶 ) “ 𝑥 ) ∈ dom vol ) → ( ( ( 𝐹𝐵 ) “ 𝑥 ) ∪ ( ( 𝐹𝐶 ) “ 𝑥 ) ) ∈ dom vol )
34 25 32 33 syl2anc ( ( 𝜑𝑥 ∈ ran (,) ) → ( ( ( 𝐹𝐵 ) “ 𝑥 ) ∪ ( ( 𝐹𝐶 ) “ 𝑥 ) ) ∈ dom vol )
35 18 34 eqeltrd ( ( 𝜑𝑥 ∈ ran (,) ) → ( 𝐹𝑥 ) ∈ dom vol )
36 35 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( 𝐹𝑥 ) ∈ dom vol )
37 ismbf ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( 𝐹𝑥 ) ∈ dom vol ) )
38 1 37 syl ( 𝜑 → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( 𝐹𝑥 ) ∈ dom vol ) )
39 36 38 mpbird ( 𝜑𝐹 ∈ MblFn )