Metamath Proof Explorer

Theorem mbfss

Description: Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses mbfss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
mbfss.2 ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
mbfss.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
mbfss.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
mbfss.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
Assertion mbfss ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 mbfss.2 ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
3 mbfss.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 mbfss.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
5 mbfss.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
6 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) )
7 undif2 ⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
8 ssequn1 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
9 1 8 sylib ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = 𝐵 )
10 7 9 syl5eq ⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
11 10 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↔ 𝑥 ∈ 𝐵 ) )
12 6 11 bitr3id ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) ↔ 𝑥 ∈ 𝐵 ) )
13 12 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) )
14 5 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
15 0cn ⊢ 0 ∈ ℂ
16 4 15 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ℂ )
17 14 16 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) ) → 𝐶 ∈ ℂ )
18 13 17 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
19 18 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
20 19 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) : 𝐵 ⟶ ℝ )
21 1 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) )
22 14 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) ) )
23 5 22 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) )
24 23 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn )
25 21 24 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ↾ 𝐴 ) ∈ MblFn )
26 difss ⊢ ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵
27 resmpt ⊢ ( ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ ( ℜ ‘ 𝐶 ) ) )
28 26 27 ax-mp ⊢ ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ ( ℜ ‘ 𝐶 ) )
29 4 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℜ ‘ 𝐶 ) = ( ℜ ‘ 0 ) )
30 re0 ⊢ ( ℜ ‘ 0 ) = 0
31 29 30 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℜ ‘ 𝐶 ) = 0 )
32 31 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ ( ℜ ‘ 𝐶 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) )
33 28 32 syl5eq ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) )
34 fconstmpt ⊢ ( ( 𝐵 ∖ 𝐴 ) × { 0 } ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 )
35 5 3 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
36 difmbl ⊢ ( ( 𝐵 ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( 𝐵 ∖ 𝐴 ) ∈ dom vol )
37 2 35 36 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ dom vol )
38 mbfconst ⊢ ( ( ( 𝐵 ∖ 𝐴 ) ∈ dom vol ∧ 0 ∈ ℂ ) → ( ( 𝐵 ∖ 𝐴 ) × { 0 } ) ∈ MblFn )
39 37 15 38 sylancl ⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝐴 ) × { 0 } ) ∈ MblFn )
40 34 39 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) ∈ MblFn )
41 33 40 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) ∈ MblFn )
42 20 25 41 10 mbfres2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn )
43 18 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
44 43 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) : 𝐵 ⟶ ℝ )
45 1 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) )
46 23 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn )
47 45 46 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ↾ 𝐴 ) ∈ MblFn )
48 resmpt ⊢ ( ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ ( ℑ ‘ 𝐶 ) ) )
49 26 48 ax-mp ⊢ ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ ( ℑ ‘ 𝐶 ) )
50 4 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℑ ‘ 𝐶 ) = ( ℑ ‘ 0 ) )
51 im0 ⊢ ( ℑ ‘ 0 ) = 0
52 50 51 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℑ ‘ 𝐶 ) = 0 )
53 52 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ ( ℑ ‘ 𝐶 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) )
54 49 53 syl5eq ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 0 ) )
55 54 40 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ↾ ( 𝐵 ∖ 𝐴 ) ) ∈ MblFn )
56 44 47 55 10 mbfres2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn )
57 18 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) ) )
58 42 56 57 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )