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 )