Metamath Proof Explorer


Theorem hsphoidmvle

Description: The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hsphoidmvle.l L=xFinax,bxifx=0kxvolakbk
hsphoidmvle.x φXFin
hsphoidmvle.z φZXY
hsphoidmvle.y X=YZ
hsphoidmvle.c φC
hsphoidmvle.h H=xcXjXifjYcjifcjxcjx
hsphoidmvle.a φA:X
hsphoidmvle.b φB:X
Assertion hsphoidmvle φALXHCBALXB

Proof

Step Hyp Ref Expression
1 hsphoidmvle.l L=xFinax,bxifx=0kxvolakbk
2 hsphoidmvle.x φXFin
3 hsphoidmvle.z φZXY
4 hsphoidmvle.y X=YZ
5 hsphoidmvle.c φC
6 hsphoidmvle.h H=xcXjXifjYcjifcjxcjx
7 hsphoidmvle.a φA:X
8 hsphoidmvle.b φB:X
9 3 eldifad φZX
10 7 9 ffvelrnd φAZ
11 8 9 ffvelrnd φBZ
12 11 5 ifcld φifBZCBZC
13 volicore AZifBZCBZCvolAZifBZCBZC
14 10 12 13 syl2anc φvolAZifBZCBZC
15 volicore AZBZvolAZBZ
16 10 11 15 syl2anc φvolAZBZ
17 difssd φXZX
18 ssfi XFinXZXXZFin
19 2 17 18 syl2anc φXZFin
20 eldifi kXZkX
21 20 adantl φkXZkX
22 7 ffvelrnda φkXAk
23 8 ffvelrnda φkXBk
24 volicore AkBkvolAkBk
25 22 23 24 syl2anc φkXvolAkBk
26 21 25 syldan φkXZvolAkBk
27 19 26 fprodrecl φkXZvolAkBk
28 nfv kφ
29 21 22 syldan φkXZAk
30 21 23 syldan φkXZBk
31 30 rexrd φkXZBk*
32 icombl AkBk*AkBkdomvol
33 29 31 32 syl2anc φkXZAkBkdomvol
34 volge0 AkBkdomvol0volAkBk
35 33 34 syl φkXZ0volAkBk
36 28 19 26 35 fprodge0 φ0kXZvolAkBk
37 12 rexrd φifBZCBZC*
38 icombl AZifBZCBZC*AZifBZCBZCdomvol
39 10 37 38 syl2anc φAZifBZCBZCdomvol
40 11 rexrd φBZ*
41 icombl AZBZ*AZBZdomvol
42 10 40 41 syl2anc φAZBZdomvol
43 10 rexrd φAZ*
44 10 leidd φAZAZ
45 min1 BZCifBZCBZCBZ
46 11 5 45 syl2anc φifBZCBZCBZ
47 icossico AZ*BZ*AZAZifBZCBZCBZAZifBZCBZCAZBZ
48 43 40 44 46 47 syl22anc φAZifBZCBZCAZBZ
49 volss AZifBZCBZCdomvolAZBZdomvolAZifBZCBZCAZBZvolAZifBZCBZCvolAZBZ
50 39 42 48 49 syl3anc φvolAZifBZCBZCvolAZBZ
51 14 16 27 36 50 lemul1ad φvolAZifBZCBZCkXZvolAkBkvolAZBZkXZvolAkBk
52 9 ne0d φX
53 6 5 2 8 hsphoif φHCB:X
54 1 2 52 7 53 hoidmvn0val φALXHCB=kXvolAkHCBk
55 53 ffvelrnda φkXHCBk
56 volicore AkHCBkvolAkHCBk
57 22 55 56 syl2anc φkXvolAkHCBk
58 57 recnd φkXvolAkHCBk
59 fveq2 k=ZAk=AZ
60 fveq2 k=ZHCBk=HCBZ
61 59 60 oveq12d k=ZAkHCBk=AZHCBZ
62 61 fveq2d k=ZvolAkHCBk=volAZHCBZ
63 62 adantl φk=ZvolAkHCBk=volAZHCBZ
64 6 5 2 8 9 hsphoival φHCBZ=ifZYBZifBZCBZC
65 3 eldifbd φ¬ZY
66 65 iffalsed φifZYBZifBZCBZC=ifBZCBZC
67 64 66 eqtrd φHCBZ=ifBZCBZC
68 67 oveq2d φAZHCBZ=AZifBZCBZC
69 68 fveq2d φvolAZHCBZ=volAZifBZCBZC
70 69 adantr φk=ZvolAZHCBZ=volAZifBZCBZC
71 63 70 eqtrd φk=ZvolAkHCBk=volAZifBZCBZC
72 2 58 9 71 fprodsplit1 φkXvolAkHCBk=volAZifBZCBZCkXZvolAkHCBk
73 5 adantr φkXZC
74 2 adantr φkXZXFin
75 8 adantr φkXZB:X
76 6 73 74 75 21 hsphoival φkXZHCBk=ifkYBkifBkCBkC
77 20 4 eleqtrdi kXZkYZ
78 eldifn kXZ¬kZ
79 elunnel2 kYZ¬kZkY
80 77 78 79 syl2anc kXZkY
81 80 adantl φkXZkY
82 81 iftrued φkXZifkYBkifBkCBkC=Bk
83 76 82 eqtrd φkXZHCBk=Bk
84 83 oveq2d φkXZAkHCBk=AkBk
85 84 fveq2d φkXZvolAkHCBk=volAkBk
86 85 prodeq2dv φkXZvolAkHCBk=kXZvolAkBk
87 86 oveq2d φvolAZifBZCBZCkXZvolAkHCBk=volAZifBZCBZCkXZvolAkBk
88 54 72 87 3eqtrd φALXHCB=volAZifBZCBZCkXZvolAkBk
89 1 7 8 2 hoidmvval φALXB=ifX=0kXvolAkBk
90 52 neneqd φ¬X=
91 90 iffalsed φifX=0kXvolAkBk=kXvolAkBk
92 25 recnd φkXvolAkBk
93 fveq2 k=ZBk=BZ
94 59 93 oveq12d k=ZAkBk=AZBZ
95 94 fveq2d k=ZvolAkBk=volAZBZ
96 95 adantl φk=ZvolAkBk=volAZBZ
97 2 92 9 96 fprodsplit1 φkXvolAkBk=volAZBZkXZvolAkBk
98 89 91 97 3eqtrd φALXB=volAZBZkXZvolAkBk
99 88 98 breq12d φALXHCBALXBvolAZifBZCBZCkXZvolAkBkvolAZBZkXZvolAkBk
100 51 99 mpbird φALXHCBALXB