Step | Hyp | Ref
| Expression |
1 | | isomennd.o |
. . . . 5
β’ (π β π:π« πβΆ(0[,]+β)) |
2 | | id 22 |
. . . . . 6
β’ (π:π« πβΆ(0[,]+β) β π:π« πβΆ(0[,]+β)) |
3 | | fdm 6682 |
. . . . . . 7
β’ (π:π« πβΆ(0[,]+β) β dom π = π« π) |
4 | 3 | feq2d 6659 |
. . . . . 6
β’ (π:π« πβΆ(0[,]+β) β (π:dom πβΆ(0[,]+β) β π:π« πβΆ(0[,]+β))) |
5 | 2, 4 | mpbird 257 |
. . . . 5
β’ (π:π« πβΆ(0[,]+β) β π:dom πβΆ(0[,]+β)) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (π β π:dom πβΆ(0[,]+β)) |
7 | | unipw 5412 |
. . . . . . 7
β’ βͺ π« π = π |
8 | 7 | pweqi 4581 |
. . . . . 6
β’ π«
βͺ π« π = π« π |
9 | 8 | a1i 11 |
. . . . 5
β’ (π β π« βͺ π« π = π« π) |
10 | 1, 3 | syl 17 |
. . . . . . 7
β’ (π β dom π = π« π) |
11 | 10 | unieqd 4884 |
. . . . . 6
β’ (π β βͺ dom π = βͺ π«
π) |
12 | 11 | pweqd 4582 |
. . . . 5
β’ (π β π« βͺ dom π = π« βͺ
π« π) |
13 | 9, 12, 10 | 3eqtr4rd 2788 |
. . . 4
β’ (π β dom π = π« βͺ
dom π) |
14 | | isomennd.o0 |
. . . 4
β’ (π β (πββ
) = 0) |
15 | 6, 13, 14 | jca31 516 |
. . 3
β’ (π β ((π:dom πβΆ(0[,]+β) β§ dom π = π« βͺ dom π) β§ (πββ
) = 0)) |
16 | | simpl 484 |
. . . . 5
β’ ((π β§ (π₯ β π« βͺ dom π β§ π¦ β π« π₯)) β π) |
17 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β π« βͺ dom π) β π₯ β π« βͺ dom π) |
18 | 12, 9 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β π« βͺ dom π = π« π) |
19 | 18 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π« βͺ dom π) β π« βͺ dom π = π« π) |
20 | 17, 19 | eleqtrd 2840 |
. . . . . . 7
β’ ((π β§ π₯ β π« βͺ dom π) β π₯ β π« π) |
21 | | elpwi 4572 |
. . . . . . 7
β’ (π₯ β π« π β π₯ β π) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β π« βͺ dom π) β π₯ β π) |
23 | 22 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β π« βͺ dom π β§ π¦ β π« π₯)) β π₯ β π) |
24 | | elpwi 4572 |
. . . . . . 7
β’ (π¦ β π« π₯ β π¦ β π₯) |
25 | 24 | adantl 483 |
. . . . . 6
β’ ((π₯ β π« βͺ dom π β§ π¦ β π« π₯) β π¦ β π₯) |
26 | 25 | adantl 483 |
. . . . 5
β’ ((π β§ (π₯ β π« βͺ dom π β§ π¦ β π« π₯)) β π¦ β π₯) |
27 | | isomennd.le |
. . . . 5
β’ ((π β§ π₯ β π β§ π¦ β π₯) β (πβπ¦) β€ (πβπ₯)) |
28 | 16, 23, 26, 27 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π₯ β π« βͺ dom π β§ π¦ β π« π₯)) β (πβπ¦) β€ (πβπ₯)) |
29 | 28 | ralrimivva 3198 |
. . 3
β’ (π β βπ₯ β π« βͺ dom πβπ¦ β π« π₯(πβπ¦) β€ (πβπ₯)) |
30 | | 0le0 12261 |
. . . . . . . . 9
β’ 0 β€
0 |
31 | 30 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ = β
) β 0 β€ 0) |
32 | | unieq 4881 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β βͺ π₯ =
βͺ β
) |
33 | | uni0 4901 |
. . . . . . . . . . . . . 14
β’ βͺ β
= β
|
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β βͺ β
= β
) |
35 | 32, 34 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π₯ = β
β βͺ π₯ =
β
) |
36 | 35 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π₯ = β
β (πββͺ π₯) =
(πββ
)) |
37 | 36 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ = β
) β (πββͺ π₯) = (πββ
)) |
38 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ = β
) β (πββ
) = 0) |
39 | 37, 38 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π₯ = β
) β (πββͺ π₯) = 0) |
40 | | reseq2 5937 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β (π βΎ π₯) = (π βΎ β
)) |
41 | | res0 5946 |
. . . . . . . . . . . . . 14
β’ (π βΎ β
) =
β
|
42 | 41 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β (π βΎ β
) =
β
) |
43 | 40, 42 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π₯ = β
β (π βΎ π₯) = β
) |
44 | 43 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π₯ = β
β
(Ξ£^β(π βΎ π₯)) =
(Ξ£^ββ
)) |
45 | | sge00 44691 |
. . . . . . . . . . . 12
β’
(Ξ£^ββ
) = 0 |
46 | 45 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ = β
β
(Ξ£^ββ
) = 0) |
47 | 44, 46 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π₯ = β
β
(Ξ£^β(π βΎ π₯)) = 0) |
48 | 47 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ = β
) β
(Ξ£^β(π βΎ π₯)) = 0) |
49 | 39, 48 | breq12d 5123 |
. . . . . . . 8
β’ ((π β§ π₯ = β
) β ((πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)) β 0 β€ 0)) |
50 | 31, 49 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π₯ = β
) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯))) |
51 | 50 | ad4ant14 751 |
. . . . . 6
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ π₯ = β
) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯))) |
52 | | simpl 484 |
. . . . . . 7
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ Β¬ π₯ = β
) β ((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο)) |
53 | | neqne 2952 |
. . . . . . . 8
β’ (Β¬
π₯ = β
β π₯ β β
) |
54 | 53 | adantl 483 |
. . . . . . 7
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ Β¬ π₯ = β
) β π₯ β β
) |
55 | | ssnnf1octb 43488 |
. . . . . . . . 9
β’ ((π₯ βΌ Ο β§ π₯ β β
) β
βπ(dom π β β β§ π:dom πβ1-1-ontoβπ₯)) |
56 | 55 | adantll 713 |
. . . . . . . 8
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ π₯ β β
) β βπ(dom π β β β§ π:dom πβ1-1-ontoβπ₯)) |
57 | 1 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β π:π« πβΆ(0[,]+β)) |
58 | 14 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β (πββ
) = 0) |
59 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π« dom π) β π₯ β π« dom π) |
60 | 10 | pweqd 4582 |
. . . . . . . . . . . . . . . 16
β’ (π β π« dom π = π« π« π) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π« dom π) β π« dom π = π« π« π) |
62 | 59, 61 | eleqtrd 2840 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π« dom π) β π₯ β π« π« π) |
63 | | elpwi 4572 |
. . . . . . . . . . . . . 14
β’ (π₯ β π« π«
π β π₯ β π« π) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π« dom π) β π₯ β π« π) |
65 | 64 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β π₯ β π« π) |
66 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π« dom π) β π) |
67 | | isomennd.sa |
. . . . . . . . . . . . . 14
β’ ((π β§ π:ββΆπ« π) β (πββͺ
π β β (πβπ)) β€
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
68 | 66, 67 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π« dom π) β§ π:ββΆπ« π) β (πββͺ
π β β (πβπ)) β€
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
69 | 68 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β§ π:ββΆπ« π) β (πββͺ
π β β (πβπ)) β€
(Ξ£^β(π β β β¦ (πβ(πβπ))))) |
70 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β dom π β β) |
71 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β π:dom πβ1-1-ontoβπ₯) |
72 | | eleq1w 2821 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β dom π β π β dom π)) |
73 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
74 | 72, 73 | ifbieq1d 4515 |
. . . . . . . . . . . . 13
β’ (π = π β if(π β dom π, (πβπ), β
) = if(π β dom π, (πβπ), β
)) |
75 | 74 | cbvmptv 5223 |
. . . . . . . . . . . 12
β’ (π β β β¦ if(π β dom π, (πβπ), β
)) = (π β β β¦ if(π β dom π, (πβπ), β
)) |
76 | 57, 58, 65, 69, 70, 71, 75 | isomenndlem 44845 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π« dom π) β§ (dom π β β β§ π:dom πβ1-1-ontoβπ₯)) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯))) |
77 | 76 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π« dom π) β ((dom π β β β§ π:dom πβ1-1-ontoβπ₯) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))) |
78 | 77 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ π₯ β β
) β ((dom π β β β§ π:dom πβ1-1-ontoβπ₯) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))) |
79 | 78 | exlimdv 1937 |
. . . . . . . 8
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ π₯ β β
) β (βπ(dom π β β β§ π:dom πβ1-1-ontoβπ₯) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))) |
80 | 56, 79 | mpd 15 |
. . . . . . 7
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ π₯ β β
) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯))) |
81 | 52, 54, 80 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β§ Β¬ π₯ = β
) β (πββͺ π₯)
β€ (Ξ£^β(π βΎ π₯))) |
82 | 51, 81 | pm2.61dan 812 |
. . . . 5
β’ (((π β§ π₯ β π« dom π) β§ π₯ βΌ Ο) β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯))) |
83 | 82 | ex 414 |
. . . 4
β’ ((π β§ π₯ β π« dom π) β (π₯ βΌ Ο β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))) |
84 | 83 | ralrimiva 3144 |
. . 3
β’ (π β βπ₯ β π« dom π(π₯ βΌ Ο β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))) |
85 | 15, 29, 84 | jca31 516 |
. 2
β’ (π β ((((π:dom πβΆ(0[,]+β) β§ dom π = π« βͺ dom π) β§ (πββ
) = 0) β§ βπ₯ β π« βͺ dom πβπ¦ β π« π₯(πβπ¦) β€ (πβπ₯)) β§ βπ₯ β π« dom π(π₯ βΌ Ο β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯))))) |
86 | | isomennd.x |
. . . . 5
β’ (π β π β π) |
87 | 86 | pwexd 5339 |
. . . 4
β’ (π β π« π β V) |
88 | 1, 87 | fexd 7182 |
. . 3
β’ (π β π β V) |
89 | | isome 44809 |
. . 3
β’ (π β V β (π β OutMeas β ((((π:dom πβΆ(0[,]+β) β§ dom π = π« βͺ dom π) β§ (πββ
) = 0) β§ βπ₯ β π« βͺ dom πβπ¦ β π« π₯(πβπ¦) β€ (πβπ₯)) β§ βπ₯ β π« dom π(π₯ βΌ Ο β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))))) |
90 | 88, 89 | syl 17 |
. 2
β’ (π β (π β OutMeas β ((((π:dom πβΆ(0[,]+β) β§ dom π = π« βͺ dom π) β§ (πββ
) = 0) β§ βπ₯ β π« βͺ dom πβπ¦ β π« π₯(πβπ¦) β€ (πβπ₯)) β§ βπ₯ β π« dom π(π₯ βΌ Ο β (πββͺ π₯) β€
(Ξ£^β(π βΎ π₯)))))) |
91 | 85, 90 | mpbird 257 |
1
β’ (π β π β OutMeas) |