Metamath Proof Explorer

Theorem hspmbl

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbl.1 
|- H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
hspmbl.x 
|- ( ph -> X e. Fin )
hspmbl.i 
|- ( ph -> K e. X )
hspmbl.y 
|- ( ph -> Y e. RR )
Assertion hspmbl 
|- ( ph -> ( K ( H ` X ) Y ) e. dom ( voln ` X ) )

Proof

Step Hyp Ref Expression
1 hspmbl.1 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
2 hspmbl.x 
 |-  ( ph -> X e. Fin )
3 hspmbl.i 
 |-  ( ph -> K e. X )
4 hspmbl.y 
 |-  ( ph -> Y e. RR )
5 2 ovnome 
 |-  ( ph -> ( voln* ` X ) e. OutMeas )
6 eqid 
 |-  U. dom ( voln* ` X ) = U. dom ( voln* ` X )
7 eqid 
 |-  ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
8 ovex 
 |-  ( -oo (,) Y ) e. _V
9 reex 
 |-  RR e. _V
10 8 9 ifex 
 |-  if ( p = K , ( -oo (,) Y ) , RR ) e. _V
11 10 ixpssmap 
 |-  X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ ( U_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) ^m X )
12 iftrue 
 |-  ( p = K -> if ( p = K , ( -oo (,) Y ) , RR ) = ( -oo (,) Y ) )
13 ioossre 
 |-  ( -oo (,) Y ) C_ RR
14 13 a1i 
 |-  ( p = K -> ( -oo (,) Y ) C_ RR )
15 12 14 eqsstrd 
 |-  ( p = K -> if ( p = K , ( -oo (,) Y ) , RR ) C_ RR )
16 iffalse 
 |-  ( -. p = K -> if ( p = K , ( -oo (,) Y ) , RR ) = RR )
17 ssid 
 |-  RR C_ RR
18 17 a1i 
 |-  ( -. p = K -> RR C_ RR )
19 16 18 eqsstrd 
 |-  ( -. p = K -> if ( p = K , ( -oo (,) Y ) , RR ) C_ RR )
20 15 19 pm2.61i 
 |-  if ( p = K , ( -oo (,) Y ) , RR ) C_ RR
21 20 rgenw 
 |-  A. p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ RR
22 iunss 
 |-  ( U_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ RR <-> A. p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ RR )
23 21 22 mpbir 
 |-  U_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ RR
24 mapss 
 |-  ( ( RR e. _V /\ U_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ RR ) -> ( U_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) ^m X ) C_ ( RR ^m X ) )
25 9 23 24 mp2an 
 |-  ( U_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) ^m X ) C_ ( RR ^m X )
26 11 25 sstri 
 |-  X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ ( RR ^m X )
27 10 rgenw 
 |-  A. p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. _V
28 ixpexg 
 |-  ( A. p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. _V -> X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. _V )
29 27 28 ax-mp 
 |-  X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. _V
30 elpwg 
 |-  ( X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. _V -> ( X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. ~P ( RR ^m X ) <-> X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ ( RR ^m X ) ) )
31 29 30 ax-mp 
 |-  ( X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. ~P ( RR ^m X ) <-> X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) C_ ( RR ^m X ) )
32 26 31 mpbir 
 |-  X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. ~P ( RR ^m X )
33 32 a1i 
 |-  ( ph -> X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. ~P ( RR ^m X ) )
34 equid 
 |-  x = x
35 eqid 
 |-  RR = RR
36 equequ1 
 |-  ( k = p -> ( k = l <-> p = l ) )
37 36 ifbid 
 |-  ( k = p -> if ( k = l , ( -oo (,) y ) , RR ) = if ( p = l , ( -oo (,) y ) , RR ) )
38 37 cbvixpv 
 |-  X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) = X_ p e. x if ( p = l , ( -oo (,) y ) , RR )
39 34 35 38 mpoeq123i 
 |-  ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) = ( l e. x , y e. RR |-> X_ p e. x if ( p = l , ( -oo (,) y ) , RR ) )
40 39 mpteq2i 
 |-  ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) ) = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ p e. x if ( p = l , ( -oo (,) y ) , RR ) ) )
41 1 40 eqtri 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ p e. x if ( p = l , ( -oo (,) y ) , RR ) ) )
42 41 2 3 4 hspval 
 |-  ( ph -> ( K ( H ` X ) Y ) = X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) )
43 2 ovnf 
 |-  ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
44 43 fdmd 
 |-  ( ph -> dom ( voln* ` X ) = ~P ( RR ^m X ) )
45 44 unieqd 
 |-  ( ph -> U. dom ( voln* ` X ) = U. ~P ( RR ^m X ) )
46 unipw 
 |-  U. ~P ( RR ^m X ) = ( RR ^m X )
47 46 a1i 
 |-  ( ph -> U. ~P ( RR ^m X ) = ( RR ^m X ) )
48 45 47 eqtrd 
 |-  ( ph -> U. dom ( voln* ` X ) = ( RR ^m X ) )
49 48 pweqd 
 |-  ( ph -> ~P U. dom ( voln* ` X ) = ~P ( RR ^m X ) )
50 42 49 eleq12d 
 |-  ( ph -> ( ( K ( H ` X ) Y ) e. ~P U. dom ( voln* ` X ) <-> X_ p e. X if ( p = K , ( -oo (,) Y ) , RR ) e. ~P ( RR ^m X ) ) )
51 33 50 mpbird 
 |-  ( ph -> ( K ( H ` X ) Y ) e. ~P U. dom ( voln* ` X ) )
52 simpl 
 |-  ( ( ph /\ a e. ~P U. dom ( voln* ` X ) ) -> ph )
53 simpr 
 |-  ( ( ph /\ a e. ~P U. dom ( voln* ` X ) ) -> a e. ~P U. dom ( voln* ` X ) )
54 52 49 syl 
 |-  ( ( ph /\ a e. ~P U. dom ( voln* ` X ) ) -> ~P U. dom ( voln* ` X ) = ~P ( RR ^m X ) )
55 53 54 eleqtrd 
 |-  ( ( ph /\ a e. ~P U. dom ( voln* ` X ) ) -> a e. ~P ( RR ^m X ) )
56 2 adantr 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> X e. Fin )
57 inss1 
 |-  ( a i^i ( K ( H ` X ) Y ) ) C_ a
58 57 a1i 
 |-  ( a e. ~P ( RR ^m X ) -> ( a i^i ( K ( H ` X ) Y ) ) C_ a )
59 elpwi 
 |-  ( a e. ~P ( RR ^m X ) -> a C_ ( RR ^m X ) )
60 58 59 sstrd 
 |-  ( a e. ~P ( RR ^m X ) -> ( a i^i ( K ( H ` X ) Y ) ) C_ ( RR ^m X ) )
61 60 adantl 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( a i^i ( K ( H ` X ) Y ) ) C_ ( RR ^m X ) )
62 56 61 ovnxrcl 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) e. RR* )
63 59 adantl 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> a C_ ( RR ^m X ) )
64 63 ssdifssd 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( a \ ( K ( H ` X ) Y ) ) C_ ( RR ^m X ) )
65 56 64 ovnxrcl 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) e. RR* )
66 62 65 xaddcld 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) e. RR* )
67 pnfge 
 |-  ( ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) e. RR* -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ +oo )
68 66 67 syl 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ +oo )
69 68 adantr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) = +oo ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ +oo )
70 id 
 |-  ( ( ( voln* ` X ) ` a ) = +oo -> ( ( voln* ` X ) ` a ) = +oo )
71 70 eqcomd 
 |-  ( ( ( voln* ` X ) ` a ) = +oo -> +oo = ( ( voln* ` X ) ` a ) )
72 71 adantl 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) = +oo ) -> +oo = ( ( voln* ` X ) ` a ) )
73 69 72 breqtrd 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) = +oo ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` a ) )
74 simpl 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ -. ( ( voln* ` X ) ` a ) = +oo ) -> ( ph /\ a e. ~P ( RR ^m X ) ) )
75 56 63 ovncl 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( ( voln* ` X ) ` a ) e. ( 0 [,] +oo ) )
76 75 adantr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ -. ( ( voln* ` X ) ` a ) = +oo ) -> ( ( voln* ` X ) ` a ) e. ( 0 [,] +oo ) )
77 neqne 
 |-  ( -. ( ( voln* ` X ) ` a ) = +oo -> ( ( voln* ` X ) ` a ) =/= +oo )
78 77 adantl 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ -. ( ( voln* ` X ) ` a ) = +oo ) -> ( ( voln* ` X ) ` a ) =/= +oo )
79 ge0xrre 
 |-  ( ( ( ( voln* ` X ) ` a ) e. ( 0 [,] +oo ) /\ ( ( voln* ` X ) ` a ) =/= +oo ) -> ( ( voln* ` X ) ` a ) e. RR )
80 76 78 79 syl2anc 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ -. ( ( voln* ` X ) ` a ) = +oo ) -> ( ( voln* ` X ) ` a ) e. RR )
81 56 adantr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) e. RR ) -> X e. Fin )
82 3 ad2antrr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) e. RR ) -> K e. X )
83 4 ad2antrr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) e. RR ) -> Y e. RR )
84 simpr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) e. RR ) -> ( ( voln* ` X ) ` a ) e. RR )
85 63 adantr 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) e. RR ) -> a C_ ( RR ^m X ) )
86 sseq1 
 |-  ( a = b -> ( a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) <-> b C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) ) )
87 86 rabbidv 
 |-  ( a = b -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } )
88 87 cbvmptv 
 |-  ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) = ( b e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | b C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } )
89 simpl 
 |-  ( ( i = h /\ p e. X ) -> i = h )
90 89 coeq2d 
 |-  ( ( i = h /\ p e. X ) -> ( [,) o. i ) = ( [,) o. h ) )
91 90 fveq1d 
 |-  ( ( i = h /\ p e. X ) -> ( ( [,) o. i ) ` p ) = ( ( [,) o. h ) ` p ) )
92 91 fveq2d 
 |-  ( ( i = h /\ p e. X ) -> ( vol ` ( ( [,) o. i ) ` p ) ) = ( vol ` ( ( [,) o. h ) ` p ) ) )
93 92 prodeq2dv 
 |-  ( i = h -> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) = prod_ p e. X ( vol ` ( ( [,) o. h ) ` p ) ) )
94 93 cbvmptv 
 |-  ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. h ) ` p ) ) )
95 fveq2 
 |-  ( n = p -> ( ( [,) o. ( m ` i ) ) ` n ) = ( ( [,) o. ( m ` i ) ) ` p ) )
96 95 cbvixpv 
 |-  X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) = X_ p e. X ( ( [,) o. ( m ` i ) ) ` p )
97 96 a1i 
 |-  ( m = h -> X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) = X_ p e. X ( ( [,) o. ( m ` i ) ) ` p ) )
98 fveq1 
 |-  ( m = h -> ( m ` i ) = ( h ` i ) )
99 98 coeq2d 
 |-  ( m = h -> ( [,) o. ( m ` i ) ) = ( [,) o. ( h ` i ) ) )
100 99 fveq1d 
 |-  ( m = h -> ( ( [,) o. ( m ` i ) ) ` p ) = ( ( [,) o. ( h ` i ) ) ` p ) )
101 100 ixpeq2dv 
 |-  ( m = h -> X_ p e. X ( ( [,) o. ( m ` i ) ) ` p ) = X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) )
102 97 101 eqtrd 
 |-  ( m = h -> X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) = X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) )
103 102 adantr 
 |-  ( ( m = h /\ i e. NN ) -> X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) = X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) )
104 103 iuneq2dv 
 |-  ( m = h -> U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) = U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) )
105 104 sseq2d 
 |-  ( m = h -> ( a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) <-> a C_ U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) ) )
106 105 cbvrabv 
 |-  { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } = { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) }
107 fveq1 
 |-  ( h = l -> ( h ` i ) = ( l ` i ) )
108 107 coeq2d 
 |-  ( h = l -> ( [,) o. ( h ` i ) ) = ( [,) o. ( l ` i ) ) )
109 108 fveq1d 
 |-  ( h = l -> ( ( [,) o. ( h ` i ) ) ` p ) = ( ( [,) o. ( l ` i ) ) ` p ) )
110 109 ixpeq2dv 
 |-  ( h = l -> X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) = X_ p e. X ( ( [,) o. ( l ` i ) ) ` p ) )
111 110 adantr 
 |-  ( ( h = l /\ i e. NN ) -> X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) = X_ p e. X ( ( [,) o. ( l ` i ) ) ` p ) )
112 111 iuneq2dv 
 |-  ( h = l -> U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) = U_ i e. NN X_ p e. X ( ( [,) o. ( l ` i ) ) ` p ) )
113 fveq2 
 |-  ( i = j -> ( l ` i ) = ( l ` j ) )
114 113 coeq2d 
 |-  ( i = j -> ( [,) o. ( l ` i ) ) = ( [,) o. ( l ` j ) ) )
115 114 fveq1d 
 |-  ( i = j -> ( ( [,) o. ( l ` i ) ) ` p ) = ( ( [,) o. ( l ` j ) ) ` p ) )
116 115 ixpeq2dv 
 |-  ( i = j -> X_ p e. X ( ( [,) o. ( l ` i ) ) ` p ) = X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) )
117 116 cbviunv 
 |-  U_ i e. NN X_ p e. X ( ( [,) o. ( l ` i ) ) ` p ) = U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p )
118 117 a1i 
 |-  ( h = l -> U_ i e. NN X_ p e. X ( ( [,) o. ( l ` i ) ) ` p ) = U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) )
119 112 118 eqtrd 
 |-  ( h = l -> U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) = U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) )
120 119 sseq2d 
 |-  ( h = l -> ( a C_ U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) <-> a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) ) )
121 120 cbvrabv 
 |-  { h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ p e. X ( ( [,) o. ( h ` i ) ) ` p ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) }
122 106 121 eqtri 
 |-  { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) }
123 122 mpteq2i 
 |-  ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } )
124 123 a1i 
 |-  ( c = b -> ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) )
125 id 
 |-  ( c = b -> c = b )
126 124 125 fveq12d 
 |-  ( c = b -> ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) = ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) )
127 126 eleq2d 
 |-  ( c = b -> ( t e. ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) <-> t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) ) )
128 2fveq3 
 |-  ( m = p -> ( vol ` ( ( [,) o. i ) ` m ) ) = ( vol ` ( ( [,) o. i ) ` p ) ) )
129 128 cbvprodv 
 |-  prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) = prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) )
130 129 mpteq2i 
 |-  ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) )
131 130 a1i 
 |-  ( m = j -> ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) = ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) )
132 fveq2 
 |-  ( m = j -> ( t ` m ) = ( t ` j ) )
133 131 132 fveq12d 
 |-  ( m = j -> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) = ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) )
134 133 cbvmptv 
 |-  ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) = ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) )
135 134 a1i 
 |-  ( c = b -> ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) = ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) )
136 135 fveq2d 
 |-  ( c = b -> ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) )
137 fveq2 
 |-  ( c = b -> ( ( voln* ` X ) ` c ) = ( ( voln* ` X ) ` b ) )
138 137 oveq1d 
 |-  ( c = b -> ( ( ( voln* ` X ) ` c ) +e s ) = ( ( ( voln* ` X ) ` b ) +e s ) )
139 136 138 breq12d 
 |-  ( c = b -> ( ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) <_ ( ( ( voln* ` X ) ` c ) +e s ) <-> ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) ) )
140 127 139 anbi12d 
 |-  ( c = b -> ( ( t e. ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) /\ ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) <_ ( ( ( voln* ` X ) ` c ) +e s ) ) <-> ( t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) /\ ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) ) ) )
141 140 rabbidva2 
 |-  ( c = b -> { t e. ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) | ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) <_ ( ( ( voln* ` X ) ` c ) +e s ) } = { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) } )
142 141 mpteq2dv 
 |-  ( c = b -> ( s e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) | ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) <_ ( ( ( voln* ` X ) ` c ) +e s ) } ) = ( s e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) } ) )
143 eqidd 
 |-  ( s = r -> ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) = ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) )
144 143 eleq2d 
 |-  ( s = r -> ( t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) <-> t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) ) )
145 oveq2 
 |-  ( s = r -> ( ( ( voln* ` X ) ` b ) +e s ) = ( ( ( voln* ` X ) ` b ) +e r ) )
146 145 breq2d 
 |-  ( s = r -> ( ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) <-> ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) ) )
147 144 146 anbi12d 
 |-  ( s = r -> ( ( t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) /\ ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) ) <-> ( t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) /\ ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) ) ) )
148 147 rabbidva2 
 |-  ( s = r -> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) } = { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) } )
149 148 cbvmptv 
 |-  ( s e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) } ) = ( r e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) } )
150 149 a1i 
 |-  ( c = b -> ( s e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e s ) } ) = ( r e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) } ) )
151 142 150 eqtrd 
 |-  ( c = b -> ( s e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) | ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) <_ ( ( ( voln* ` X ) ` c ) +e s ) } ) = ( r e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) } ) )
152 151 cbvmptv 
 |-  ( c e. ~P ( RR ^m X ) |-> ( s e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { m e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ i e. NN X_ n e. X ( ( [,) o. ( m ` i ) ) ` n ) } ) ` c ) | ( sum^ ` ( m e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ m e. X ( vol ` ( ( [,) o. i ) ` m ) ) ) ` ( t ` m ) ) ) ) <_ ( ( ( voln* ` X ) ` c ) +e s ) } ) ) = ( b e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { t e. ( ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ p e. X ( ( [,) o. ( l ` j ) ) ` p ) } ) ` b ) | ( sum^ ` ( j e. NN |-> ( ( i e. ( ( RR X. RR ) ^m X ) |-> prod_ p e. X ( vol ` ( ( [,) o. i ) ` p ) ) ) ` ( t ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` b ) +e r ) } ) )
153 2fveq3 
 |-  ( m = p -> ( 1st ` ( ( t ` j ) ` m ) ) = ( 1st ` ( ( t ` j ) ` p ) ) )
154 153 cbvmptv 
 |-  ( m e. X |-> ( 1st ` ( ( t ` j ) ` m ) ) ) = ( p e. X |-> ( 1st ` ( ( t ` j ) ` p ) ) )
155 154 mpteq2i 
 |-  ( j e. NN |-> ( m e. X |-> ( 1st ` ( ( t ` j ) ` m ) ) ) ) = ( j e. NN |-> ( p e. X |-> ( 1st ` ( ( t ` j ) ` p ) ) ) )
156 fveq2 
 |-  ( i = j -> ( t ` i ) = ( t ` j ) )
157 156 fveq1d 
 |-  ( i = j -> ( ( t ` i ) ` m ) = ( ( t ` j ) ` m ) )
158 157 fveq2d 
 |-  ( i = j -> ( 2nd ` ( ( t ` i ) ` m ) ) = ( 2nd ` ( ( t ` j ) ` m ) ) )
159 158 mpteq2dv 
 |-  ( i = j -> ( m e. X |-> ( 2nd ` ( ( t ` i ) ` m ) ) ) = ( m e. X |-> ( 2nd ` ( ( t ` j ) ` m ) ) ) )
160 2fveq3 
 |-  ( m = p -> ( 2nd ` ( ( t ` j ) ` m ) ) = ( 2nd ` ( ( t ` j ) ` p ) ) )
161 160 cbvmptv 
 |-  ( m e. X |-> ( 2nd ` ( ( t ` j ) ` m ) ) ) = ( p e. X |-> ( 2nd ` ( ( t ` j ) ` p ) ) )
162 161 a1i 
 |-  ( i = j -> ( m e. X |-> ( 2nd ` ( ( t ` j ) ` m ) ) ) = ( p e. X |-> ( 2nd ` ( ( t ` j ) ` p ) ) ) )
163 159 162 eqtrd 
 |-  ( i = j -> ( m e. X |-> ( 2nd ` ( ( t ` i ) ` m ) ) ) = ( p e. X |-> ( 2nd ` ( ( t ` j ) ` p ) ) ) )
164 163 cbvmptv 
 |-  ( i e. NN |-> ( m e. X |-> ( 2nd ` ( ( t ` i ) ` m ) ) ) ) = ( j e. NN |-> ( p e. X |-> ( 2nd ` ( ( t ` j ) ` p ) ) ) )
165 41 81 82 83 84 85 88 94 152 155 164 hspmbllem3 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ ( ( voln* ` X ) ` a ) e. RR ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` a ) )
166 74 80 165 syl2anc 
 |-  ( ( ( ph /\ a e. ~P ( RR ^m X ) ) /\ -. ( ( voln* ` X ) ` a ) = +oo ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` a ) )
167 73 166 pm2.61dan 
 |-  ( ( ph /\ a e. ~P ( RR ^m X ) ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` a ) )
168 52 55 167 syl2anc 
 |-  ( ( ph /\ a e. ~P U. dom ( voln* ` X ) ) -> ( ( ( voln* ` X ) ` ( a i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( a \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` a ) )
169 5 6 7 51 168 caragenel2d 
 |-  ( ph -> ( K ( H ` X ) Y ) e. ( CaraGen ` ( voln* ` X ) ) )
170 2 dmvon 
 |-  ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
171 170 eqcomd 
 |-  ( ph -> ( CaraGen ` ( voln* ` X ) ) = dom ( voln ` X ) )
172 169 171 eleqtrd 
 |-  ( ph -> ( K ( H ` X ) Y ) e. dom ( voln ` X ) )