Step | Hyp | Ref
| Expression |
1 | | hsphoidmvle.a |
. . . . 5
β’ (π β π΄:πβΆβ) |
2 | | hsphoidmvle.z |
. . . . . 6
β’ (π β π β (π β π)) |
3 | 2 | eldifad 3959 |
. . . . 5
β’ (π β π β π) |
4 | 1, 3 | ffvelcdmd 7083 |
. . . 4
β’ (π β (π΄βπ) β β) |
5 | | hsphoidmvle.b |
. . . . . 6
β’ (π β π΅:πβΆβ) |
6 | 5, 3 | ffvelcdmd 7083 |
. . . . 5
β’ (π β (π΅βπ) β β) |
7 | | hsphoidmvle.c |
. . . . 5
β’ (π β πΆ β β) |
8 | 6, 7 | ifcld 4573 |
. . . 4
β’ (π β if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β β) |
9 | | volicore 45232 |
. . . 4
β’ (((π΄βπ) β β β§ if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β β) β (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) β β) |
10 | 4, 8, 9 | syl2anc 585 |
. . 3
β’ (π β (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) β β) |
11 | | volicore 45232 |
. . . 4
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
12 | 4, 6, 11 | syl2anc 585 |
. . 3
β’ (π β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
13 | | hsphoidmvle.x |
. . . . 5
β’ (π β π β Fin) |
14 | | difssd 4131 |
. . . . 5
β’ (π β (π β {π}) β π) |
15 | | ssfi 9169 |
. . . . 5
β’ ((π β Fin β§ (π β {π}) β π) β (π β {π}) β Fin) |
16 | 13, 14, 15 | syl2anc 585 |
. . . 4
β’ (π β (π β {π}) β Fin) |
17 | | eldifi 4125 |
. . . . . 6
β’ (π β (π β {π}) β π β π) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((π β§ π β (π β {π})) β π β π) |
19 | 1 | ffvelcdmda 7082 |
. . . . . 6
β’ ((π β§ π β π) β (π΄βπ) β β) |
20 | 5 | ffvelcdmda 7082 |
. . . . . 6
β’ ((π β§ π β π) β (π΅βπ) β β) |
21 | | volicore 45232 |
. . . . . 6
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
23 | 18, 22 | syldan 592 |
. . . 4
β’ ((π β§ π β (π β {π})) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
24 | 16, 23 | fprodrecl 15893 |
. . 3
β’ (π β βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))) β β) |
25 | | nfv 1918 |
. . . 4
β’
β²ππ |
26 | 18, 19 | syldan 592 |
. . . . . 6
β’ ((π β§ π β (π β {π})) β (π΄βπ) β β) |
27 | 18, 20 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β (π β {π})) β (π΅βπ) β β) |
28 | 27 | rexrd 11260 |
. . . . . 6
β’ ((π β§ π β (π β {π})) β (π΅βπ) β
β*) |
29 | | icombl 25063 |
. . . . . 6
β’ (((π΄βπ) β β β§ (π΅βπ) β β*) β ((π΄βπ)[,)(π΅βπ)) β dom vol) |
30 | 26, 28, 29 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β (π β {π})) β ((π΄βπ)[,)(π΅βπ)) β dom vol) |
31 | | volge0 44612 |
. . . . 5
β’ (((π΄βπ)[,)(π΅βπ)) β dom vol β 0 β€
(volβ((π΄βπ)[,)(π΅βπ)))) |
32 | 30, 31 | syl 17 |
. . . 4
β’ ((π β§ π β (π β {π})) β 0 β€ (volβ((π΄βπ)[,)(π΅βπ)))) |
33 | 25, 16, 23, 32 | fprodge0 15933 |
. . 3
β’ (π β 0 β€ βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) |
34 | 8 | rexrd 11260 |
. . . . 5
β’ (π β if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β
β*) |
35 | | icombl 25063 |
. . . . 5
β’ (((π΄βπ) β β β§ if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β β*) β ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) β dom vol) |
36 | 4, 34, 35 | syl2anc 585 |
. . . 4
β’ (π β ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) β dom vol) |
37 | 6 | rexrd 11260 |
. . . . 5
β’ (π β (π΅βπ) β
β*) |
38 | | icombl 25063 |
. . . . 5
β’ (((π΄βπ) β β β§ (π΅βπ) β β*) β ((π΄βπ)[,)(π΅βπ)) β dom vol) |
39 | 4, 37, 38 | syl2anc 585 |
. . . 4
β’ (π β ((π΄βπ)[,)(π΅βπ)) β dom vol) |
40 | 4 | rexrd 11260 |
. . . . 5
β’ (π β (π΄βπ) β
β*) |
41 | 4 | leidd 11776 |
. . . . 5
β’ (π β (π΄βπ) β€ (π΄βπ)) |
42 | | min1 13164 |
. . . . . 6
β’ (((π΅βπ) β β β§ πΆ β β) β if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β€ (π΅βπ)) |
43 | 6, 7, 42 | syl2anc 585 |
. . . . 5
β’ (π β if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β€ (π΅βπ)) |
44 | | icossico 13390 |
. . . . 5
β’ ((((π΄βπ) β β* β§ (π΅βπ) β β*) β§ ((π΄βπ) β€ (π΄βπ) β§ if((π΅βπ) β€ πΆ, (π΅βπ), πΆ) β€ (π΅βπ))) β ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) β ((π΄βπ)[,)(π΅βπ))) |
45 | 40, 37, 41, 43, 44 | syl22anc 838 |
. . . 4
β’ (π β ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) β ((π΄βπ)[,)(π΅βπ))) |
46 | | volss 25032 |
. . . 4
β’ ((((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) β dom vol β§ ((π΄βπ)[,)(π΅βπ)) β dom vol β§ ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) β ((π΄βπ)[,)(π΅βπ))) β (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) β€ (volβ((π΄βπ)[,)(π΅βπ)))) |
47 | 36, 39, 45, 46 | syl3anc 1372 |
. . 3
β’ (π β (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) β€ (volβ((π΄βπ)[,)(π΅βπ)))) |
48 | 10, 12, 24, 33, 47 | lemul1ad 12149 |
. 2
β’ (π β ((volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) β€ ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
49 | | hsphoidmvle.l |
. . . . 5
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
50 | 3 | ne0d 4334 |
. . . . 5
β’ (π β π β β
) |
51 | | hsphoidmvle.h |
. . . . . 6
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
52 | 51, 7, 13, 5 | hsphoif 45227 |
. . . . 5
β’ (π β ((π»βπΆ)βπ΅):πβΆβ) |
53 | 49, 13, 50, 1, 52 | hoidmvn0val 45235 |
. . . 4
β’ (π β (π΄(πΏβπ)((π»βπΆ)βπ΅)) = βπ β π (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)))) |
54 | 52 | ffvelcdmda 7082 |
. . . . . . 7
β’ ((π β§ π β π) β (((π»βπΆ)βπ΅)βπ) β β) |
55 | | volicore 45232 |
. . . . . . 7
β’ (((π΄βπ) β β β§ (((π»βπΆ)βπ΅)βπ) β β) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) β β) |
56 | 19, 54, 55 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) β β) |
57 | 56 | recnd 11238 |
. . . . 5
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) β β) |
58 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = π β (π΄βπ) = (π΄βπ)) |
59 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = π β (((π»βπΆ)βπ΅)βπ) = (((π»βπΆ)βπ΅)βπ)) |
60 | 58, 59 | oveq12d 7422 |
. . . . . . . 8
β’ (π = π β ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)) = ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) |
61 | 60 | fveq2d 6892 |
. . . . . . 7
β’ (π = π β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)))) |
62 | 61 | adantl 483 |
. . . . . 6
β’ ((π β§ π = π) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)))) |
63 | 51, 7, 13, 5, 3 | hsphoival 45230 |
. . . . . . . . . 10
β’ (π β (((π»βπΆ)βπ΅)βπ) = if(π β π, (π΅βπ), if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) |
64 | 2 | eldifbd 3960 |
. . . . . . . . . . 11
β’ (π β Β¬ π β π) |
65 | 64 | iffalsed 4538 |
. . . . . . . . . 10
β’ (π β if(π β π, (π΅βπ), if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) = if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) |
66 | 63, 65 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (((π»βπΆ)βπ΅)βπ) = if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) |
67 | 66 | oveq2d 7420 |
. . . . . . . 8
β’ (π β ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)) = ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) |
68 | 67 | fveq2d 6892 |
. . . . . . 7
β’ (π β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)))) |
69 | 68 | adantr 482 |
. . . . . 6
β’ ((π β§ π = π) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)))) |
70 | 62, 69 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π = π) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = (volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)))) |
71 | 13, 57, 3, 70 | fprodsplit1 44244 |
. . . 4
β’ (π β βπ β π (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = ((volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))))) |
72 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {π})) β πΆ β β) |
73 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {π})) β π β Fin) |
74 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {π})) β π΅:πβΆβ) |
75 | 51, 72, 73, 74, 18 | hsphoival 45230 |
. . . . . . . . 9
β’ ((π β§ π β (π β {π})) β (((π»βπΆ)βπ΅)βπ) = if(π β π, (π΅βπ), if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) |
76 | | hsphoidmvle.y |
. . . . . . . . . . . . 13
β’ π = (π βͺ {π}) |
77 | 17, 76 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π β (π β {π}) β π β (π βͺ {π})) |
78 | | eldifn 4126 |
. . . . . . . . . . . 12
β’ (π β (π β {π}) β Β¬ π β {π}) |
79 | | elunnel2 4149 |
. . . . . . . . . . . 12
β’ ((π β (π βͺ {π}) β§ Β¬ π β {π}) β π β π) |
80 | 77, 78, 79 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π β {π}) β π β π) |
81 | 80 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {π})) β π β π) |
82 | 81 | iftrued 4535 |
. . . . . . . . 9
β’ ((π β§ π β (π β {π})) β if(π β π, (π΅βπ), if((π΅βπ) β€ πΆ, (π΅βπ), πΆ)) = (π΅βπ)) |
83 | 75, 82 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β (π β {π})) β (((π»βπΆ)βπ΅)βπ) = (π΅βπ)) |
84 | 83 | oveq2d 7420 |
. . . . . . 7
β’ ((π β§ π β (π β {π})) β ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)) = ((π΄βπ)[,)(π΅βπ))) |
85 | 84 | fveq2d 6892 |
. . . . . 6
β’ ((π β§ π β (π β {π})) β (volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
86 | 85 | prodeq2dv 15863 |
. . . . 5
β’ (π β βπ β (π β {π})(volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ))) = βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) |
87 | 86 | oveq2d 7420 |
. . . 4
β’ (π β ((volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(((π»βπΆ)βπ΅)βπ)))) = ((volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
88 | 53, 71, 87 | 3eqtrd 2777 |
. . 3
β’ (π β (π΄(πΏβπ)((π»βπΆ)βπ΅)) = ((volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
89 | 49, 1, 5, 13 | hoidmvval 45228 |
. . . 4
β’ (π β (π΄(πΏβπ)π΅) = if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ))))) |
90 | 50 | neneqd 2946 |
. . . . 5
β’ (π β Β¬ π = β
) |
91 | 90 | iffalsed 4538 |
. . . 4
β’ (π β if(π = β
, 0, βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
92 | 22 | recnd 11238 |
. . . . 5
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
93 | | fveq2 6888 |
. . . . . . . 8
β’ (π = π β (π΅βπ) = (π΅βπ)) |
94 | 58, 93 | oveq12d 7422 |
. . . . . . 7
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
95 | 94 | fveq2d 6892 |
. . . . . 6
β’ (π = π β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
96 | 95 | adantl 483 |
. . . . 5
β’ ((π β§ π = π) β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
97 | 13, 92, 3, 96 | fprodsplit1 44244 |
. . . 4
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
98 | 89, 91, 97 | 3eqtrd 2777 |
. . 3
β’ (π β (π΄(πΏβπ)π΅) = ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ))))) |
99 | 88, 98 | breq12d 5160 |
. 2
β’ (π β ((π΄(πΏβπ)((π»βπΆ)βπ΅)) β€ (π΄(πΏβπ)π΅) β ((volβ((π΄βπ)[,)if((π΅βπ) β€ πΆ, (π΅βπ), πΆ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))) β€ ((volβ((π΄βπ)[,)(π΅βπ))) Β· βπ β (π β {π})(volβ((π΄βπ)[,)(π΅βπ)))))) |
100 | 48, 99 | mpbird 257 |
1
β’ (π β (π΄(πΏβπ)((π»βπΆ)βπ΅)) β€ (π΄(πΏβπ)π΅)) |