Step | Hyp | Ref
| Expression |
1 | | elun 4109 |
. . . . . . . 8
β’ (π₯ β (π΄ βͺ (π΅ β π΄)) β (π₯ β π΄ β¨ π₯ β (π΅ β π΄))) |
2 | | undif2 4437 |
. . . . . . . . . 10
β’ (π΄ βͺ (π΅ β π΄)) = (π΄ βͺ π΅) |
3 | | mbfss.1 |
. . . . . . . . . . 11
β’ (π β π΄ β π΅) |
4 | | ssequn1 4141 |
. . . . . . . . . . 11
β’ (π΄ β π΅ β (π΄ βͺ π΅) = π΅) |
5 | 3, 4 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π΄ βͺ π΅) = π΅) |
6 | 2, 5 | eqtrid 2789 |
. . . . . . . . 9
β’ (π β (π΄ βͺ (π΅ β π΄)) = π΅) |
7 | 6 | eleq2d 2824 |
. . . . . . . 8
β’ (π β (π₯ β (π΄ βͺ (π΅ β π΄)) β π₯ β π΅)) |
8 | 1, 7 | bitr3id 285 |
. . . . . . 7
β’ (π β ((π₯ β π΄ β¨ π₯ β (π΅ β π΄)) β π₯ β π΅)) |
9 | 8 | biimpar 479 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β (π₯ β π΄ β¨ π₯ β (π΅ β π΄))) |
10 | | mbfss.5 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) |
11 | | mbfss.3 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β πΆ β π) |
12 | 10, 11 | mbfmptcl 25003 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β πΆ β β) |
13 | | mbfss.4 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ = 0) |
14 | | 0cn 11148 |
. . . . . . . 8
β’ 0 β
β |
15 | 13, 14 | eqeltrdi 2846 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅ β π΄)) β πΆ β β) |
16 | 12, 15 | jaodan 957 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¨ π₯ β (π΅ β π΄))) β πΆ β β) |
17 | 9, 16 | syldan 592 |
. . . . 5
β’ ((π β§ π₯ β π΅) β πΆ β β) |
18 | 17 | recld 15080 |
. . . 4
β’ ((π β§ π₯ β π΅) β (ββπΆ) β β) |
19 | 18 | fmpttd 7064 |
. . 3
β’ (π β (π₯ β π΅ β¦ (ββπΆ)):π΅βΆβ) |
20 | 3 | resmptd 5995 |
. . . 4
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ π΄) = (π₯ β π΄ β¦ (ββπΆ))) |
21 | 12 | ismbfcn2 25005 |
. . . . . 6
β’ (π β ((π₯ β π΄ β¦ πΆ) β MblFn β ((π₯ β π΄ β¦ (ββπΆ)) β MblFn β§ (π₯ β π΄ β¦ (ββπΆ)) β MblFn))) |
22 | 10, 21 | mpbid 231 |
. . . . 5
β’ (π β ((π₯ β π΄ β¦ (ββπΆ)) β MblFn β§ (π₯ β π΄ β¦ (ββπΆ)) β MblFn)) |
23 | 22 | simpld 496 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββπΆ)) β MblFn) |
24 | 20, 23 | eqeltrd 2838 |
. . 3
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ π΄) β MblFn) |
25 | | difss 4092 |
. . . . . 6
β’ (π΅ β π΄) β π΅ |
26 | | resmpt 5992 |
. . . . . 6
β’ ((π΅ β π΄) β π΅ β ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) = (π₯ β (π΅ β π΄) β¦ (ββπΆ))) |
27 | 25, 26 | ax-mp 5 |
. . . . 5
β’ ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) = (π₯ β (π΅ β π΄) β¦ (ββπΆ)) |
28 | 13 | fveq2d 6847 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅ β π΄)) β (ββπΆ) = (ββ0)) |
29 | | re0 15038 |
. . . . . . 7
β’
(ββ0) = 0 |
30 | 28, 29 | eqtrdi 2793 |
. . . . . 6
β’ ((π β§ π₯ β (π΅ β π΄)) β (ββπΆ) = 0) |
31 | 30 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π₯ β (π΅ β π΄) β¦ (ββπΆ)) = (π₯ β (π΅ β π΄) β¦ 0)) |
32 | 27, 31 | eqtrid 2789 |
. . . 4
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) = (π₯ β (π΅ β π΄) β¦ 0)) |
33 | | fconstmpt 5695 |
. . . . 5
β’ ((π΅ β π΄) Γ {0}) = (π₯ β (π΅ β π΄) β¦ 0) |
34 | | mbfss.2 |
. . . . . . 7
β’ (π β π΅ β dom vol) |
35 | 10, 11 | mbfdm2 25004 |
. . . . . . 7
β’ (π β π΄ β dom vol) |
36 | | difmbl 24910 |
. . . . . . 7
β’ ((π΅ β dom vol β§ π΄ β dom vol) β (π΅ β π΄) β dom vol) |
37 | 34, 35, 36 | syl2anc 585 |
. . . . . 6
β’ (π β (π΅ β π΄) β dom vol) |
38 | | mbfconst 25000 |
. . . . . 6
β’ (((π΅ β π΄) β dom vol β§ 0 β β)
β ((π΅ β π΄) Γ {0}) β
MblFn) |
39 | 37, 14, 38 | sylancl 587 |
. . . . 5
β’ (π β ((π΅ β π΄) Γ {0}) β
MblFn) |
40 | 33, 39 | eqeltrrid 2843 |
. . . 4
β’ (π β (π₯ β (π΅ β π΄) β¦ 0) β MblFn) |
41 | 32, 40 | eqeltrd 2838 |
. . 3
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) β MblFn) |
42 | 19, 24, 41, 6 | mbfres2 25012 |
. 2
β’ (π β (π₯ β π΅ β¦ (ββπΆ)) β MblFn) |
43 | 17 | imcld 15081 |
. . . 4
β’ ((π β§ π₯ β π΅) β (ββπΆ) β β) |
44 | 43 | fmpttd 7064 |
. . 3
β’ (π β (π₯ β π΅ β¦ (ββπΆ)):π΅βΆβ) |
45 | 3 | resmptd 5995 |
. . . 4
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ π΄) = (π₯ β π΄ β¦ (ββπΆ))) |
46 | 22 | simprd 497 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββπΆ)) β MblFn) |
47 | 45, 46 | eqeltrd 2838 |
. . 3
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ π΄) β MblFn) |
48 | | resmpt 5992 |
. . . . . 6
β’ ((π΅ β π΄) β π΅ β ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) = (π₯ β (π΅ β π΄) β¦ (ββπΆ))) |
49 | 25, 48 | ax-mp 5 |
. . . . 5
β’ ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) = (π₯ β (π΅ β π΄) β¦ (ββπΆ)) |
50 | 13 | fveq2d 6847 |
. . . . . . 7
β’ ((π β§ π₯ β (π΅ β π΄)) β (ββπΆ) = (ββ0)) |
51 | | im0 15039 |
. . . . . . 7
β’
(ββ0) = 0 |
52 | 50, 51 | eqtrdi 2793 |
. . . . . 6
β’ ((π β§ π₯ β (π΅ β π΄)) β (ββπΆ) = 0) |
53 | 52 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π₯ β (π΅ β π΄) β¦ (ββπΆ)) = (π₯ β (π΅ β π΄) β¦ 0)) |
54 | 49, 53 | eqtrid 2789 |
. . . 4
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) = (π₯ β (π΅ β π΄) β¦ 0)) |
55 | 54, 40 | eqeltrd 2838 |
. . 3
β’ (π β ((π₯ β π΅ β¦ (ββπΆ)) βΎ (π΅ β π΄)) β MblFn) |
56 | 44, 47, 55, 6 | mbfres2 25012 |
. 2
β’ (π β (π₯ β π΅ β¦ (ββπΆ)) β MblFn) |
57 | 17 | ismbfcn2 25005 |
. 2
β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β ((π₯ β π΅ β¦ (ββπΆ)) β MblFn β§ (π₯ β π΅ β¦ (ββπΆ)) β MblFn))) |
58 | 42, 56, 57 | mpbir2and 712 |
1
β’ (π β (π₯ β π΅ β¦ πΆ) β MblFn) |