Metamath Proof Explorer

Theorem sge0hsphoire

Description: If the generalized sum of dimensional volumes of n-dimensional half-open intervals is finite, then the sum stays finite if every half-open interval is intersected with a half-space. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0hsphoire.l 
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
sge0hsphoire.f 
|- ( ph -> Y e. Fin )
sge0hsphoire.z 
|- ( ph -> Z e. ( W \ Y ) )
sge0hsphoire.w 
|- W = ( Y u. { Z } )
sge0hsphoire.c 
|- ( ph -> C : NN --> ( RR ^m W ) )
sge0hsphoire.d 
|- ( ph -> D : NN --> ( RR ^m W ) )
sge0hsphoire.r 
|- ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
sge0hsphoire.h 
|- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
sge0hsphoire.s 
|- ( ph -> S e. RR )
Assertion sge0hsphoire 
|- ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 sge0hsphoire.l 
 |-  L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
2 sge0hsphoire.f 
 |-  ( ph -> Y e. Fin )
3 sge0hsphoire.z 
 |-  ( ph -> Z e. ( W \ Y ) )
4 sge0hsphoire.w 
 |-  W = ( Y u. { Z } )
5 sge0hsphoire.c 
 |-  ( ph -> C : NN --> ( RR ^m W ) )
6 sge0hsphoire.d 
 |-  ( ph -> D : NN --> ( RR ^m W ) )
7 sge0hsphoire.r 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
8 sge0hsphoire.h 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
9 sge0hsphoire.s 
 |-  ( ph -> S e. RR )
10 nnex 
 |-  NN e. _V
11 10 a1i 
 |-  ( ph -> NN e. _V )
12 snfi 
 |-  { Z } e. Fin
13 12 a1i 
 |-  ( ph -> { Z } e. Fin )
14 unfi 
 |-  ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
15 2 13 14 syl2anc 
 |-  ( ph -> ( Y u. { Z } ) e. Fin )
16 4 15 eqeltrid 
 |-  ( ph -> W e. Fin )
17 16 adantr 
 |-  ( ( ph /\ j e. NN ) -> W e. Fin )
18 5 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
19 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
20 18 19 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
21 eleq1w 
 |-  ( j = h -> ( j e. Y <-> h e. Y ) )
22 fveq2 
 |-  ( j = h -> ( c ` j ) = ( c ` h ) )
23 22 breq1d 
 |-  ( j = h -> ( ( c ` j ) <_ x <-> ( c ` h ) <_ x ) )
24 23 22 ifbieq1d 
 |-  ( j = h -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` h ) <_ x , ( c ` h ) , x ) )
25 21 22 24 ifbieq12d 
 |-  ( j = h -> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) = if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) )
26 25 cbvmptv 
 |-  ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) = ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) )
27 26 mpteq2i 
 |-  ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) = ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) )
28 27 mpteq2i 
 |-  ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) ) = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) ) )
29 8 28 eqtri 
 |-  H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( h e. W |-> if ( h e. Y , ( c ` h ) , if ( ( c ` h ) <_ x , ( c ` h ) , x ) ) ) ) )
30 9 adantr 
 |-  ( ( ph /\ j e. NN ) -> S e. RR )
31 6 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
32 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
33 31 32 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
34 29 30 17 33 hsphoif 
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` S ) ` ( D ` j ) ) : W --> RR )
35 1 17 20 34 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
36 eqid 
 |-  ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
37 35 36 fmptd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) : NN --> ( 0 [,) +oo ) )
38 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
39 38 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
40 37 39 fssd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) : NN --> ( 0 [,] +oo ) )
41 11 40 sge0cl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) )
42 11 40 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR* )
43 pnfxr 
 |-  +oo e. RR*
44 43 a1i 
 |-  ( ph -> +oo e. RR* )
45 7 rexrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR* )
46 nfv 
 |-  F/ j ph
47 38 35 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
48 1 17 20 33 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,) +oo ) )
49 38 48 sseldi 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( D ` j ) ) e. ( 0 [,] +oo ) )
50 3 adantr 
 |-  ( ( ph /\ j e. NN ) -> Z e. ( W \ Y ) )
51 1 17 50 4 30 29 20 33 hsphoidmvle 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) <_ ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
52 46 11 47 49 51 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
53 7 ltpnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) < +oo )
54 42 45 44 52 53 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) < +oo )
55 42 44 54 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) =/= +oo )
56 ge0xrre 
 |-  ( ( ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. ( 0 [,] +oo ) /\ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) =/= +oo ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
57 41 55 56 syl2anc 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )