Proof of Theorem mbfss
Step | Hyp | Ref
| Expression |
1 | | elun 3753 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐴)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴))) |
2 | | undif2 4044 |
. . . . . . . . . 10
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
3 | | mbfss.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
4 | | ssequn1 3783 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
5 | 3, 4 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝐵) |
6 | 2, 5 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) |
7 | 6 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ 𝐵)) |
8 | 1, 7 | syl5bbr 274 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴)) ↔ 𝑥 ∈ 𝐵)) |
9 | 8 | biimpar 502 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴))) |
10 | | mbfss.5 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) |
11 | | mbfss.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
12 | 10, 11 | mbfmptcl 23404 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
13 | | mbfss.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) |
14 | | 0cn 10032 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
15 | 13, 14 | syl6eqel 2709 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ) |
16 | 12, 15 | jaodan 826 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ (𝐵 ∖ 𝐴))) → 𝐶 ∈ ℂ) |
17 | 9, 16 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
18 | 17 | recld 13934 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘𝐶) ∈ ℝ) |
19 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) = (𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) |
20 | 18, 19 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)):𝐵⟶ℝ) |
21 | 3 | resmptd 5452 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))) |
22 | 12 | ismbfcn2 23406 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) ∈ MblFn))) |
23 | 10, 22 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) ∈ MblFn)) |
24 | 23 | simpld 475 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)) ∈ MblFn) |
25 | 21, 24 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ↾ 𝐴) ∈ MblFn) |
26 | | difss 3737 |
. . . . . 6
⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵 |
27 | | resmpt 5449 |
. . . . . 6
⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ (ℜ‘𝐶))) |
28 | 26, 27 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ (ℜ‘𝐶)) |
29 | 13 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → (ℜ‘𝐶) = (ℜ‘0)) |
30 | | re0 13892 |
. . . . . . 7
⊢
(ℜ‘0) = 0 |
31 | 29, 30 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → (ℜ‘𝐶) = 0) |
32 | 31 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ (ℜ‘𝐶)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ 0)) |
33 | 28, 32 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ 0)) |
34 | | fconstmpt 5163 |
. . . . 5
⊢ ((𝐵 ∖ 𝐴) × {0}) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ 0) |
35 | | mbfss.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ dom vol) |
36 | 10, 11 | mbfdm2 23405 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ dom vol) |
37 | | difmbl 23311 |
. . . . . . 7
⊢ ((𝐵 ∈ dom vol ∧ 𝐴 ∈ dom vol) → (𝐵 ∖ 𝐴) ∈ dom vol) |
38 | 35, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝐴) ∈ dom vol) |
39 | | mbfconst 23402 |
. . . . . 6
⊢ (((𝐵 ∖ 𝐴) ∈ dom vol ∧ 0 ∈ ℂ)
→ ((𝐵 ∖ 𝐴) × {0}) ∈
MblFn) |
40 | 38, 14, 39 | sylancl 694 |
. . . . 5
⊢ (𝜑 → ((𝐵 ∖ 𝐴) × {0}) ∈
MblFn) |
41 | 34, 40 | syl5eqelr 2706 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ 0) ∈ MblFn) |
42 | 33, 41 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) ∈ MblFn) |
43 | 20, 25, 42, 6 | mbfres2 23412 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ∈ MblFn) |
44 | 17 | imcld 13935 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℑ‘𝐶) ∈ ℝ) |
45 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) = (𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) |
46 | 44, 45 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)):𝐵⟶ℝ) |
47 | 3 | resmptd 5452 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))) |
48 | 23 | simprd 479 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)) ∈ MblFn) |
49 | 47, 48 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ↾ 𝐴) ∈ MblFn) |
50 | | resmpt 5449 |
. . . . . 6
⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ (ℑ‘𝐶))) |
51 | 26, 50 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ (ℑ‘𝐶)) |
52 | 13 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → (ℑ‘𝐶) = (ℑ‘0)) |
53 | | im0 13893 |
. . . . . . 7
⊢
(ℑ‘0) = 0 |
54 | 52, 53 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → (ℑ‘𝐶) = 0) |
55 | 54 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ (ℑ‘𝐶)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ 0)) |
56 | 51, 55 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) = (𝑥 ∈ (𝐵 ∖ 𝐴) ↦ 0)) |
57 | 56, 41 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ↾ (𝐵 ∖ 𝐴)) ∈ MblFn) |
58 | 46, 49, 57, 6 | mbfres2 23412 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ∈ MblFn) |
59 | 17 | ismbfcn2 23406 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ ((𝑥 ∈ 𝐵 ↦ (ℜ‘𝐶)) ∈ MblFn ∧ (𝑥 ∈ 𝐵 ↦ (ℑ‘𝐶)) ∈ MblFn))) |
60 | 43, 58, 59 | mpbir2and 957 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) |