Step | Hyp | Ref
| Expression |
1 | | hspmbl.x |
. . . 4
β’ (π β π β Fin) |
2 | 1 | ovnome 45337 |
. . 3
β’ (π β (voln*βπ) β
OutMeas) |
3 | | eqid 2733 |
. . 3
β’ βͺ dom (voln*βπ) = βͺ dom
(voln*βπ) |
4 | | eqid 2733 |
. . 3
β’
(CaraGenβ(voln*βπ)) = (CaraGenβ(voln*βπ)) |
5 | | ovex 7442 |
. . . . . . . . 9
β’
(-β(,)π)
β V |
6 | | reex 11201 |
. . . . . . . . 9
β’ β
β V |
7 | 5, 6 | ifex 4579 |
. . . . . . . 8
β’ if(π = πΎ, (-β(,)π), β) β V |
8 | 7 | ixpssmap 8926 |
. . . . . . 7
β’ Xπ β
π if(π = πΎ, (-β(,)π), β) β (βͺ π β π if(π = πΎ, (-β(,)π), β) βm π) |
9 | | iftrue 4535 |
. . . . . . . . . . . 12
β’ (π = πΎ β if(π = πΎ, (-β(,)π), β) = (-β(,)π)) |
10 | | ioossre 13385 |
. . . . . . . . . . . . 13
β’
(-β(,)π)
β β |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
β’ (π = πΎ β (-β(,)π) β β) |
12 | 9, 11 | eqsstrd 4021 |
. . . . . . . . . . 11
β’ (π = πΎ β if(π = πΎ, (-β(,)π), β) β
β) |
13 | | iffalse 4538 |
. . . . . . . . . . . 12
β’ (Β¬
π = πΎ β if(π = πΎ, (-β(,)π), β) = β) |
14 | | ssid 4005 |
. . . . . . . . . . . . 13
β’ β
β β |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
β’ (Β¬
π = πΎ β β β
β) |
16 | 13, 15 | eqsstrd 4021 |
. . . . . . . . . . 11
β’ (Β¬
π = πΎ β if(π = πΎ, (-β(,)π), β) β
β) |
17 | 12, 16 | pm2.61i 182 |
. . . . . . . . . 10
β’ if(π = πΎ, (-β(,)π), β) β β |
18 | 17 | rgenw 3066 |
. . . . . . . . 9
β’
βπ β
π if(π = πΎ, (-β(,)π), β) β β |
19 | | iunss 5049 |
. . . . . . . . 9
β’ (βͺ π β π if(π = πΎ, (-β(,)π), β) β β β
βπ β π if(π = πΎ, (-β(,)π), β) β
β) |
20 | 18, 19 | mpbir 230 |
. . . . . . . 8
β’ βͺ π β π if(π = πΎ, (-β(,)π), β) β β |
21 | | mapss 8883 |
. . . . . . . 8
β’ ((β
β V β§ βͺ π β π if(π = πΎ, (-β(,)π), β) β β) β
(βͺ π β π if(π = πΎ, (-β(,)π), β) βm π) β (β
βm π)) |
22 | 6, 20, 21 | mp2an 691 |
. . . . . . 7
β’ (βͺ π β π if(π = πΎ, (-β(,)π), β) βm π) β (β
βm π) |
23 | 8, 22 | sstri 3992 |
. . . . . 6
β’ Xπ β
π if(π = πΎ, (-β(,)π), β) β (β
βm π) |
24 | 7 | rgenw 3066 |
. . . . . . . 8
β’
βπ β
π if(π = πΎ, (-β(,)π), β) β V |
25 | | ixpexg 8916 |
. . . . . . . 8
β’
(βπ β
π if(π = πΎ, (-β(,)π), β) β V β Xπ β
π if(π = πΎ, (-β(,)π), β) β V) |
26 | 24, 25 | ax-mp 5 |
. . . . . . 7
β’ Xπ β
π if(π = πΎ, (-β(,)π), β) β V |
27 | | elpwg 4606 |
. . . . . . 7
β’ (Xπ β
π if(π = πΎ, (-β(,)π), β) β V β (Xπ β
π if(π = πΎ, (-β(,)π), β) β π« (β
βm π)
β Xπ β π if(π = πΎ, (-β(,)π), β) β (β
βm π))) |
28 | 26, 27 | ax-mp 5 |
. . . . . 6
β’ (Xπ β
π if(π = πΎ, (-β(,)π), β) β π« (β
βm π)
β Xπ β π if(π = πΎ, (-β(,)π), β) β (β
βm π)) |
29 | 23, 28 | mpbir 230 |
. . . . 5
β’ Xπ β
π if(π = πΎ, (-β(,)π), β) β π« (β
βm π) |
30 | 29 | a1i 11 |
. . . 4
β’ (π β Xπ β
π if(π = πΎ, (-β(,)π), β) β π« (β
βm π)) |
31 | | hspmbl.1 |
. . . . . . 7
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
32 | | equid 2016 |
. . . . . . . . 9
β’ π₯ = π₯ |
33 | | eqid 2733 |
. . . . . . . . 9
β’ β =
β |
34 | | equequ1 2029 |
. . . . . . . . . . 11
β’ (π = π β (π = π β π = π)) |
35 | 34 | ifbid 4552 |
. . . . . . . . . 10
β’ (π = π β if(π = π, (-β(,)π¦), β) = if(π = π, (-β(,)π¦), β)) |
36 | 35 | cbvixpv 8909 |
. . . . . . . . 9
β’ Xπ β
π₯ if(π = π, (-β(,)π¦), β) = Xπ β π₯ if(π = π, (-β(,)π¦), β) |
37 | 32, 33, 36 | mpoeq123i 7485 |
. . . . . . . 8
β’ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β)) = (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β)) |
38 | 37 | mpteq2i 5254 |
. . . . . . 7
β’ (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
39 | 31, 38 | eqtri 2761 |
. . . . . 6
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
40 | | hspmbl.i |
. . . . . 6
β’ (π β πΎ β π) |
41 | | hspmbl.y |
. . . . . 6
β’ (π β π β β) |
42 | 39, 1, 40, 41 | hspval 45373 |
. . . . 5
β’ (π β (πΎ(π»βπ)π) = Xπ β π if(π = πΎ, (-β(,)π), β)) |
43 | 1 | ovnf 45327 |
. . . . . . . . 9
β’ (π β (voln*βπ):π« (β
βm π)βΆ(0[,]+β)) |
44 | 43 | fdmd 6729 |
. . . . . . . 8
β’ (π β dom (voln*βπ) = π« (β
βm π)) |
45 | 44 | unieqd 4923 |
. . . . . . 7
β’ (π β βͺ dom (voln*βπ) = βͺ π«
(β βm π)) |
46 | | unipw 5451 |
. . . . . . . 8
β’ βͺ π« (β βm π) = (β βm π) |
47 | 46 | a1i 11 |
. . . . . . 7
β’ (π β βͺ π« (β βm π) = (β βm π)) |
48 | 45, 47 | eqtrd 2773 |
. . . . . 6
β’ (π β βͺ dom (voln*βπ) = (β βm π)) |
49 | 48 | pweqd 4620 |
. . . . 5
β’ (π β π« βͺ dom (voln*βπ) = π« (β βm
π)) |
50 | 42, 49 | eleq12d 2828 |
. . . 4
β’ (π β ((πΎ(π»βπ)π) β π« βͺ dom (voln*βπ) β Xπ β π if(π = πΎ, (-β(,)π), β) β π« (β
βm π))) |
51 | 30, 50 | mpbird 257 |
. . 3
β’ (π β (πΎ(π»βπ)π) β π« βͺ dom (voln*βπ)) |
52 | | simpl 484 |
. . . 4
β’ ((π β§ π β π« βͺ dom (voln*βπ)) β π) |
53 | | simpr 486 |
. . . . 5
β’ ((π β§ π β π« βͺ dom (voln*βπ)) β π β π« βͺ dom (voln*βπ)) |
54 | 52, 49 | syl 17 |
. . . . 5
β’ ((π β§ π β π« βͺ dom (voln*βπ)) β π« βͺ dom (voln*βπ) = π« (β βm
π)) |
55 | 53, 54 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π β π« βͺ dom (voln*βπ)) β π β π« (β βm
π)) |
56 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π« (β βm
π)) β π β Fin) |
57 | | inss1 4229 |
. . . . . . . . . . . . 13
β’ (π β© (πΎ(π»βπ)π)) β π |
58 | 57 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π« (β
βm π)
β (π β© (πΎ(π»βπ)π)) β π) |
59 | | elpwi 4610 |
. . . . . . . . . . . 12
β’ (π β π« (β
βm π)
β π β (β
βm π)) |
60 | 58, 59 | sstrd 3993 |
. . . . . . . . . . 11
β’ (π β π« (β
βm π)
β (π β© (πΎ(π»βπ)π)) β (β βm π)) |
61 | 60 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β π« (β βm
π)) β (π β© (πΎ(π»βπ)π)) β (β βm π)) |
62 | 56, 61 | ovnxrcl 45333 |
. . . . . . . . 9
β’ ((π β§ π β π« (β βm
π)) β
((voln*βπ)β(π β© (πΎ(π»βπ)π))) β
β*) |
63 | 59 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β π« (β βm
π)) β π β (β
βm π)) |
64 | 63 | ssdifssd 4143 |
. . . . . . . . . 10
β’ ((π β§ π β π« (β βm
π)) β (π β (πΎ(π»βπ)π)) β (β βm π)) |
65 | 56, 64 | ovnxrcl 45333 |
. . . . . . . . 9
β’ ((π β§ π β π« (β βm
π)) β
((voln*βπ)β(π β (πΎ(π»βπ)π))) β
β*) |
66 | 62, 65 | xaddcld 13280 |
. . . . . . . 8
β’ ((π β§ π β π« (β βm
π)) β
(((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β
β*) |
67 | | pnfge 13110 |
. . . . . . . 8
β’
((((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β β* β
(((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ +β) |
68 | 66, 67 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π« (β βm
π)) β
(((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ +β) |
69 | 68 | adantr 482 |
. . . . . 6
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) = +β) β (((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ +β) |
70 | | id 22 |
. . . . . . . 8
β’
(((voln*βπ)βπ) = +β β ((voln*βπ)βπ) = +β) |
71 | 70 | eqcomd 2739 |
. . . . . . 7
β’
(((voln*βπ)βπ) = +β β +β =
((voln*βπ)βπ)) |
72 | 71 | adantl 483 |
. . . . . 6
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) = +β) β +β =
((voln*βπ)βπ)) |
73 | 69, 72 | breqtrd 5175 |
. . . . 5
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) = +β) β (((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ ((voln*βπ)βπ)) |
74 | | simpl 484 |
. . . . . 6
β’ (((π β§ π β π« (β βm
π)) β§ Β¬
((voln*βπ)βπ) = +β) β (π β§ π β π« (β βm
π))) |
75 | 56, 63 | ovncl 45331 |
. . . . . . . 8
β’ ((π β§ π β π« (β βm
π)) β
((voln*βπ)βπ) β (0[,]+β)) |
76 | 75 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§ Β¬
((voln*βπ)βπ) = +β) β ((voln*βπ)βπ) β (0[,]+β)) |
77 | | neqne 2949 |
. . . . . . . 8
β’ (Β¬
((voln*βπ)βπ) = +β β ((voln*βπ)βπ) β +β) |
78 | 77 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§ Β¬
((voln*βπ)βπ) = +β) β ((voln*βπ)βπ) β +β) |
79 | | ge0xrre 44292 |
. . . . . . 7
β’
((((voln*βπ)βπ) β (0[,]+β) β§
((voln*βπ)βπ) β +β) β ((voln*βπ)βπ) β β) |
80 | 76, 78, 79 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β π« (β βm
π)) β§ Β¬
((voln*βπ)βπ) = +β) β ((voln*βπ)βπ) β β) |
81 | 56 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) β β) β π β Fin) |
82 | 40 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) β β) β πΎ β π) |
83 | 41 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) β β) β π β β) |
84 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) β β) β ((voln*βπ)βπ) β β) |
85 | 63 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) β β) β π β (β βm π)) |
86 | | sseq1 4008 |
. . . . . . . . 9
β’ (π = π β (π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ))) |
87 | 86 | rabbidv 3441 |
. . . . . . . 8
β’ (π = π β {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)} = {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)}) |
88 | 87 | cbvmptv 5262 |
. . . . . . 7
β’ (π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) = (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) |
89 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π = β β§ π β π) β π = β) |
90 | 89 | coeq2d 5863 |
. . . . . . . . . . 11
β’ ((π = β β§ π β π) β ([,) β π) = ([,) β β)) |
91 | 90 | fveq1d 6894 |
. . . . . . . . . 10
β’ ((π = β β§ π β π) β (([,) β π)βπ) = (([,) β β)βπ)) |
92 | 91 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π = β β§ π β π) β (volβ(([,) β π)βπ)) = (volβ(([,) β β)βπ))) |
93 | 92 | prodeq2dv 15867 |
. . . . . . . 8
β’ (π = β β βπ β π (volβ(([,) β π)βπ)) = βπ β π (volβ(([,) β β)βπ))) |
94 | 93 | cbvmptv 5262 |
. . . . . . 7
β’ (π β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β π)βπ))) = (β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ))) |
95 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (([,) β (πβπ))βπ) = (([,) β (πβπ))βπ)) |
96 | 95 | cbvixpv 8909 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ Xπ β
π (([,) β (πβπ))βπ) = Xπ β π (([,) β (πβπ))βπ) |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β β Xπ β π (([,) β (πβπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
98 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = β β (πβπ) = (ββπ)) |
99 | 98 | coeq2d 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = β β ([,) β (πβπ)) = ([,) β (ββπ))) |
100 | 99 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = β β (([,) β (πβπ))βπ) = (([,) β (ββπ))βπ)) |
101 | 100 | ixpeq2dv 8907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β β Xπ β π (([,) β (πβπ))βπ) = Xπ β π (([,) β (ββπ))βπ)) |
102 | 97, 101 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β β Xπ β π (([,) β (πβπ))βπ) = Xπ β π (([,) β (ββπ))βπ)) |
103 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = β β§ π β β) β Xπ β
π (([,) β (πβπ))βπ) = Xπ β π (([,) β (ββπ))βπ)) |
104 | 103 | iuneq2dv 5022 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π (([,) β (ββπ))βπ)) |
105 | 104 | sseq2d 4015 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β β (π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ))) |
106 | 105 | cbvrabv 3443 |
. . . . . . . . . . . . . . . . 17
β’ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)} = {β β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ)} |
107 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (β = π β (ββπ) = (πβπ)) |
108 | 107 | coeq2d 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (β = π β ([,) β (ββπ)) = ([,) β (πβπ))) |
109 | 108 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β = π β (([,) β (ββπ))βπ) = (([,) β (πβπ))βπ)) |
110 | 109 | ixpeq2dv 8907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β = π β Xπ β π (([,) β (ββπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
111 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β = π β§ π β β) β Xπ β
π (([,) β (ββπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
112 | 111 | iuneq2dv 5022 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) = βͺ π β β Xπ β
π (([,) β (πβπ))βπ)) |
113 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (πβπ) = (πβπ)) |
114 | 113 | coeq2d 5863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β ([,) β (πβπ)) = ([,) β (πβπ))) |
115 | 114 | fveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (([,) β (πβπ))βπ) = (([,) β (πβπ))βπ)) |
116 | 115 | ixpeq2dv 8907 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β Xπ β π (([,) β (πβπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
117 | 116 | cbviunv 5044 |
. . . . . . . . . . . . . . . . . . . . 21
β’ βͺ π β β Xπ β π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π (([,) β (πβπ))βπ) |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π (([,) β (πβπ))βπ)) |
119 | 112, 118 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) = βͺ π β β Xπ β
π (([,) β (πβπ))βπ)) |
120 | 119 | sseq2d 4015 |
. . . . . . . . . . . . . . . . . 18
β’ (β = π β (π β βͺ
π β β Xπ β
π (([,) β (ββπ))βπ) β π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ))) |
121 | 120 | cbvrabv 3443 |
. . . . . . . . . . . . . . . . 17
β’ {β β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (ββπ))βπ)} = {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)} |
122 | 106, 121 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)} = {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)} |
123 | 122 | mpteq2i 5254 |
. . . . . . . . . . . . . . 15
β’ (π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) = (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) = (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})) |
125 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
126 | 124, 125 | fveq12d 6899 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) = ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ)) |
127 | 126 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π = π β (π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ))) |
128 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (volβ(([,) β π)βπ)) = (volβ(([,) β π)βπ))) |
129 | 128 | cbvprodv 15860 |
. . . . . . . . . . . . . . . . . . 19
β’
βπ β
π (volβ(([,) β
π)βπ)) = βπ β π (volβ(([,) β π)βπ)) |
130 | 129 | mpteq2i 5254 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β π)βπ))) = (π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ))) |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ))) = (π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))) |
132 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π‘βπ) = (π‘βπ)) |
133 | 131, 132 | fveq12d 6899 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)) = ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ))) |
134 | 133 | cbvmptv 5262 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ ((π β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β π)βπ)))β(π‘βπ))) = (π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ))) |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ))) = (π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) |
136 | 135 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (π = π β
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) =
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ))))) |
137 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = π β ((voln*βπ)βπ) = ((voln*βπ)βπ)) |
138 | 137 | oveq1d 7424 |
. . . . . . . . . . . . 13
β’ (π = π β (((voln*βπ)βπ) +π π ) = (((voln*βπ)βπ) +π π )) |
139 | 136, 138 | breq12d 5162 |
. . . . . . . . . . . 12
β’ (π = π β
((Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π ) β
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π ))) |
140 | 127, 139 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = π β ((π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β§
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )) β (π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β§
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )))) |
141 | 140 | rabbidva2 3435 |
. . . . . . . . . 10
β’ (π = π β {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )} = {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )}) |
142 | 141 | mpteq2dv 5251 |
. . . . . . . . 9
β’ (π = π β (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )}) = (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )})) |
143 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) = ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ)) |
144 | 143 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’ (π = π β (π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ))) |
145 | | oveq2 7417 |
. . . . . . . . . . . . . 14
β’ (π = π β (((voln*βπ)βπ) +π π ) = (((voln*βπ)βπ) +π π)) |
146 | 145 | breq2d 5161 |
. . . . . . . . . . . . 13
β’ (π = π β
((Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π ) β
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π))) |
147 | 144, 146 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = π β ((π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β§
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )) β (π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β§
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π)))) |
148 | 147 | rabbidva2 3435 |
. . . . . . . . . . 11
β’ (π = π β {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )} = {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π)}) |
149 | 148 | cbvmptv 5262 |
. . . . . . . . . 10
β’ (π β β+
β¦ {π‘ β ((π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )}) = (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π)}) |
150 | 149 | a1i 11 |
. . . . . . . . 9
β’ (π = π β (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )}) = (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π)})) |
151 | 142, 150 | eqtrd 2773 |
. . . . . . . 8
β’ (π = π β (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )}) = (π β β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π)})) |
152 | 151 | cbvmptv 5262 |
. . . . . . 7
β’ (π β π« (β
βm π)
β¦ (π β
β+ β¦ {π‘ β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π )})) = (π β π« (β βm
π) β¦ (π β β+
β¦ {π‘ β ((π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ)))β(π‘βπ)))) β€ (((voln*βπ)βπ) +π π)})) |
153 | | 2fveq3 6897 |
. . . . . . . . 9
β’ (π = π β (1st β((π‘βπ)βπ)) = (1st β((π‘βπ)βπ))) |
154 | 153 | cbvmptv 5262 |
. . . . . . . 8
β’ (π β π β¦ (1st β((π‘βπ)βπ))) = (π β π β¦ (1st β((π‘βπ)βπ))) |
155 | 154 | mpteq2i 5254 |
. . . . . . 7
β’ (π β β β¦ (π β π β¦ (1st β((π‘βπ)βπ)))) = (π β β β¦ (π β π β¦ (1st β((π‘βπ)βπ)))) |
156 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = π β (π‘βπ) = (π‘βπ)) |
157 | 156 | fveq1d 6894 |
. . . . . . . . . . 11
β’ (π = π β ((π‘βπ)βπ) = ((π‘βπ)βπ)) |
158 | 157 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π = π β (2nd β((π‘βπ)βπ)) = (2nd β((π‘βπ)βπ))) |
159 | 158 | mpteq2dv 5251 |
. . . . . . . . 9
β’ (π = π β (π β π β¦ (2nd β((π‘βπ)βπ))) = (π β π β¦ (2nd β((π‘βπ)βπ)))) |
160 | | 2fveq3 6897 |
. . . . . . . . . . 11
β’ (π = π β (2nd β((π‘βπ)βπ)) = (2nd β((π‘βπ)βπ))) |
161 | 160 | cbvmptv 5262 |
. . . . . . . . . 10
β’ (π β π β¦ (2nd β((π‘βπ)βπ))) = (π β π β¦ (2nd β((π‘βπ)βπ))) |
162 | 161 | a1i 11 |
. . . . . . . . 9
β’ (π = π β (π β π β¦ (2nd β((π‘βπ)βπ))) = (π β π β¦ (2nd β((π‘βπ)βπ)))) |
163 | 159, 162 | eqtrd 2773 |
. . . . . . . 8
β’ (π = π β (π β π β¦ (2nd β((π‘βπ)βπ))) = (π β π β¦ (2nd β((π‘βπ)βπ)))) |
164 | 163 | cbvmptv 5262 |
. . . . . . 7
β’ (π β β β¦ (π β π β¦ (2nd β((π‘βπ)βπ)))) = (π β β β¦ (π β π β¦ (2nd β((π‘βπ)βπ)))) |
165 | 39, 81, 82, 83, 84, 85, 88, 94, 152, 155, 164 | hspmbllem3 45392 |
. . . . . 6
β’ (((π β§ π β π« (β βm
π)) β§
((voln*βπ)βπ) β β) β (((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ ((voln*βπ)βπ)) |
166 | 74, 80, 165 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β π« (β βm
π)) β§ Β¬
((voln*βπ)βπ) = +β) β (((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ ((voln*βπ)βπ)) |
167 | 73, 166 | pm2.61dan 812 |
. . . 4
β’ ((π β§ π β π« (β βm
π)) β
(((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ ((voln*βπ)βπ)) |
168 | 52, 55, 167 | syl2anc 585 |
. . 3
β’ ((π β§ π β π« βͺ dom (voln*βπ)) β (((voln*βπ)β(π β© (πΎ(π»βπ)π))) +π
((voln*βπ)β(π β (πΎ(π»βπ)π)))) β€ ((voln*βπ)βπ)) |
169 | 2, 3, 4, 51, 168 | caragenel2d 45296 |
. 2
β’ (π β (πΎ(π»βπ)π) β (CaraGenβ(voln*βπ))) |
170 | 1 | dmvon 45370 |
. . 3
β’ (π β dom (volnβπ) =
(CaraGenβ(voln*βπ))) |
171 | 170 | eqcomd 2739 |
. 2
β’ (π β
(CaraGenβ(voln*βπ)) = dom (volnβπ)) |
172 | 169, 171 | eleqtrd 2836 |
1
β’ (π β (πΎ(π»βπ)π) β dom (volnβπ)) |