Metamath Proof Explorer

Theorem ovnhoilem2

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoilem2.x 
|- ( ph -> X e. Fin )
ovnhoilem2.n 
|- ( ph -> X =/= (/) )
ovnhoilem2.a 
|- ( ph -> A : X --> RR )
ovnhoilem2.b 
|- ( ph -> B : X --> RR )
ovnhoilem2.i 
|- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
ovnhoilem2.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 ) ) ) ) ) )
ovnhoilem2.m 
|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
ovnhoilem2.f 
|- F = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )
ovnhoilem2.s 
|- S = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )
Assertion ovnhoilem2 
|- ( ph -> ( A ( L ` X ) B ) <_ ( ( voln* ` X ) ` I ) )

Proof

Step Hyp Ref Expression
1 ovnhoilem2.x 
 |-  ( ph -> X e. Fin )
2 ovnhoilem2.n 
 |-  ( ph -> X =/= (/) )
3 ovnhoilem2.a 
 |-  ( ph -> A : X --> RR )
4 ovnhoilem2.b 
 |-  ( ph -> B : X --> RR )
5 ovnhoilem2.i 
 |-  I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
6 ovnhoilem2.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 ) ) ) ) ) )
7 ovnhoilem2.m 
 |-  M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
8 ovnhoilem2.f 
 |-  F = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )
9 ovnhoilem2.s 
 |-  S = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )
10 7 eleq2i 
 |-  ( z e. M <-> z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )
11 rabid 
 |-  ( z e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } <-> ( z e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
12 10 11 bitri 
 |-  ( z e. M <-> ( z e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
13 12 biimpi 
 |-  ( z e. M -> ( z e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
14 13 simprd 
 |-  ( z e. M -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
15 14 adantl 
 |-  ( ( ph /\ z e. M ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
16 1 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> X e. Fin )
17 3 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> A : X --> RR )
18 4 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> B : X --> RR )
19 elmapi 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) )
20 19 ffvelrnda 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( i ` n ) e. ( ( RR X. RR ) ^m X ) )
21 elmapi 
 |-  ( ( i ` n ) e. ( ( RR X. RR ) ^m X ) -> ( i ` n ) : X --> ( RR X. RR ) )
22 20 21 syl 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( i ` n ) : X --> ( RR X. RR ) )
23 22 ffvelrnda 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ l e. X ) -> ( ( i ` n ) ` l ) e. ( RR X. RR ) )
24 xp1st 
 |-  ( ( ( i ` n ) ` l ) e. ( RR X. RR ) -> ( 1st ` ( ( i ` n ) ` l ) ) e. RR )
25 23 24 syl 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ l e. X ) -> ( 1st ` ( ( i ` n ) ` l ) ) e. RR )
26 25 fmpttd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) : X --> RR )
27 reex 
 |-  RR e. _V
28 27 a1i 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> RR e. _V )
29 1nn 
 |-  1 e. NN
30 29 a1i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> 1 e. NN )
31 19 30 ffvelrnd 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( i ` 1 ) e. ( ( RR X. RR ) ^m X ) )
32 elmapex 
 |-  ( ( i ` 1 ) e. ( ( RR X. RR ) ^m X ) -> ( ( RR X. RR ) e. _V /\ X e. _V ) )
33 32 simprd 
 |-  ( ( i ` 1 ) e. ( ( RR X. RR ) ^m X ) -> X e. _V )
34 31 33 syl 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> X e. _V )
35 34 adantr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> X e. _V )
36 elmapg 
 |-  ( ( RR e. _V /\ X e. _V ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. ( RR ^m X ) <-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) : X --> RR ) )
37 28 35 36 syl2anc 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. ( RR ^m X ) <-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) : X --> RR ) )
38 26 37 mpbird 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. ( RR ^m X ) )
39 38 fmpttd 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) : NN --> ( RR ^m X ) )
40 id 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
41 nnex 
 |-  NN e. _V
42 41 mptex 
 |-  ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) e. _V
43 42 a1i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) e. _V )
44 8 fvmpt2 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) e. _V ) -> ( F ` i ) = ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )
45 40 43 44 syl2anc 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( F ` i ) = ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )
46 45 feq1d 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( ( F ` i ) : NN --> ( RR ^m X ) <-> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) : NN --> ( RR ^m X ) ) )
47 39 46 mpbird 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( F ` i ) : NN --> ( RR ^m X ) )
48 47 3ad2ant2 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( F ` i ) : NN --> ( RR ^m X ) )
49 xp2nd 
 |-  ( ( ( i ` n ) ` l ) e. ( RR X. RR ) -> ( 2nd ` ( ( i ` n ) ` l ) ) e. RR )
50 23 49 syl 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ l e. X ) -> ( 2nd ` ( ( i ` n ) ` l ) ) e. RR )
51 50 fmpttd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) : X --> RR )
52 elmapg 
 |-  ( ( RR e. _V /\ X e. _V ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. ( RR ^m X ) <-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) : X --> RR ) )
53 28 35 52 syl2anc 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. ( RR ^m X ) <-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) : X --> RR ) )
54 51 53 mpbird 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. ( RR ^m X ) )
55 54 fmpttd 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) : NN --> ( RR ^m X ) )
56 41 mptex 
 |-  ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) e. _V
57 56 a1i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) e. _V )
58 9 fvmpt2 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) e. _V ) -> ( S ` i ) = ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )
59 40 57 58 syl2anc 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( S ` i ) = ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )
60 59 feq1d 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( ( S ` i ) : NN --> ( RR ^m X ) <-> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) : NN --> ( RR ^m X ) ) )
61 55 60 mpbird 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( S ` i ) : NN --> ( RR ^m X ) )
62 61 3ad2ant2 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( S ` i ) : NN --> ( RR ^m X ) )
63 simp3 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
64 5 a1i 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
65 fveq2 
 |-  ( j = n -> ( i ` j ) = ( i ` n ) )
66 65 fveq1d 
 |-  ( j = n -> ( ( i ` j ) ` k ) = ( ( i ` n ) ` k ) )
67 66 fveq2d 
 |-  ( j = n -> ( 1st ` ( ( i ` j ) ` k ) ) = ( 1st ` ( ( i ` n ) ` k ) ) )
68 66 fveq2d 
 |-  ( j = n -> ( 2nd ` ( ( i ` j ) ` k ) ) = ( 2nd ` ( ( i ` n ) ` k ) ) )
69 67 68 oveq12d 
 |-  ( j = n -> ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) = ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) ) )
70 69 ixpeq2dv 
 |-  ( j = n -> X_ k e. X ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) = X_ k e. X ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) ) )
71 70 cbviunv 
 |-  U_ j e. NN X_ k e. X ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) = U_ n e. NN X_ k e. X ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) )
72 71 a1i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> U_ j e. NN X_ k e. X ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) = U_ n e. NN X_ k e. X ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) ) )
73 19 ffvelrnda 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> ( i ` j ) e. ( ( RR X. RR ) ^m X ) )
74 elmapi 
 |-  ( ( i ` j ) e. ( ( RR X. RR ) ^m X ) -> ( i ` j ) : X --> ( RR X. RR ) )
75 73 74 syl 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> ( i ` j ) : X --> ( RR X. RR ) )
76 75 adantr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) /\ k e. X ) -> ( i ` j ) : X --> ( RR X. RR ) )
77 simpr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) /\ k e. X ) -> k e. X )
78 76 77 fvovco 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) )
79 78 ixpeq2dva 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) )
80 79 iuneq2dv 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) )
81 simpl 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
82 42 a1i 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) e. _V )
83 81 82 44 syl2anc 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( F ` i ) = ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )
84 83 fveq1d 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( F ` i ) ` n ) = ( ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) ` n ) )
85 simpr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> n e. NN )
86 mptexg 
 |-  ( X e. _V -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. _V )
87 34 86 syl 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. _V )
88 87 adantr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. _V )
89 eqid 
 |-  ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) = ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
90 89 fvmpt2 
 |-  ( ( n e. NN /\ ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) e. _V ) -> ( ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) ` n ) = ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
91 85 88 90 syl2anc 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) ` n ) = ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
92 84 91 eqtrd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( F ` i ) ` n ) = ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
93 92 fveq1d 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( ( F ` i ) ` n ) ` k ) = ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) )
94 93 adantr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( ( F ` i ) ` n ) ` k ) = ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) )
95 eqidd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) = ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
96 simpr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) /\ l = k ) -> l = k )
97 96 fveq2d 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) /\ l = k ) -> ( ( i ` n ) ` l ) = ( ( i ` n ) ` k ) )
98 97 fveq2d 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) /\ l = k ) -> ( 1st ` ( ( i ` n ) ` l ) ) = ( 1st ` ( ( i ` n ) ` k ) ) )
99 simpr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> k e. X )
100 fvexd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> ( 1st ` ( ( i ` n ) ` k ) ) e. _V )
101 95 98 99 100 fvmptd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) = ( 1st ` ( ( i ` n ) ` k ) ) )
102 101 adantlr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) = ( 1st ` ( ( i ` n ) ` k ) ) )
103 94 102 eqtrd 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( ( F ` i ) ` n ) ` k ) = ( 1st ` ( ( i ` n ) ` k ) ) )
104 59 fveq1d 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( ( S ` i ) ` n ) = ( ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) ` n ) )
105 104 adantr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( S ` i ) ` n ) = ( ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) ` n ) )
106 mptexg 
 |-  ( X e. _V -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. _V )
107 34 106 syl 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. _V )
108 107 adantr 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. _V )
109 eqid 
 |-  ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) = ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
110 109 fvmpt2 
 |-  ( ( n e. NN /\ ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) e. _V ) -> ( ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) ` n ) = ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
111 85 108 110 syl2anc 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) ` n ) = ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
112 105 111 eqtrd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( S ` i ) ` n ) = ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
113 112 fveq1d 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> ( ( ( S ` i ) ` n ) ` k ) = ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) )
114 113 adantr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( ( S ` i ) ` n ) ` k ) = ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) )
115 eqidd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) = ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
116 2fveq3 
 |-  ( l = k -> ( 2nd ` ( ( i ` n ) ` l ) ) = ( 2nd ` ( ( i ` n ) ` k ) ) )
117 116 adantl 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) /\ l = k ) -> ( 2nd ` ( ( i ` n ) ` l ) ) = ( 2nd ` ( ( i ` n ) ` k ) ) )
118 fvexd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> ( 2nd ` ( ( i ` n ) ` k ) ) e. _V )
119 115 117 99 118 fvmptd 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ k e. X ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) = ( 2nd ` ( ( i ` n ) ` k ) ) )
120 119 adantlr 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) = ( 2nd ` ( ( i ` n ) ` k ) ) )
121 114 120 eqtrd 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( ( S ` i ) ` n ) ` k ) = ( 2nd ` ( ( i ` n ) ` k ) ) )
122 103 121 oveq12d 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) /\ k e. X ) -> ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) = ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) ) )
123 122 ixpeq2dva 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ n e. NN ) -> X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) = X_ k e. X ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) ) )
124 123 iuneq2dv 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) = U_ n e. NN X_ k e. X ( ( 1st ` ( ( i ` n ) ` k ) ) [,) ( 2nd ` ( ( i ` n ) ` k ) ) ) )
125 72 80 124 3eqtr4d 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) )
126 125 adantl 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) )
127 126 3adant3 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) )
128 64 127 sseq12d 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) ) )
129 63 128 mpbid 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) )
130 129 3adant3r 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ n e. NN X_ k e. X ( ( ( ( F ` i ) ` n ) ` k ) [,) ( ( ( S ` i ) ` n ) ` k ) ) )
131 6 16 17 18 48 62 130 hoidmvle 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( n e. NN |-> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) ) ) )
132 simpl 
 |-  ( ( n = j /\ l e. X ) -> n = j )
133 132 fveq2d 
 |-  ( ( n = j /\ l e. X ) -> ( i ` n ) = ( i ` j ) )
134 133 fveq1d 
 |-  ( ( n = j /\ l e. X ) -> ( ( i ` n ) ` l ) = ( ( i ` j ) ` l ) )
135 134 fveq2d 
 |-  ( ( n = j /\ l e. X ) -> ( 1st ` ( ( i ` n ) ` l ) ) = ( 1st ` ( ( i ` j ) ` l ) ) )
136 135 mpteq2dva 
 |-  ( n = j -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) = ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) )
137 136 fveq1d 
 |-  ( n = j -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) = ( ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) ` k ) )
138 137 adantr 
 |-  ( ( n = j /\ k e. X ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) = ( ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) ` k ) )
139 eqidd 
 |-  ( k e. X -> ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) = ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) )
140 2fveq3 
 |-  ( l = k -> ( 1st ` ( ( i ` j ) ` l ) ) = ( 1st ` ( ( i ` j ) ` k ) ) )
141 140 adantl 
 |-  ( ( k e. X /\ l = k ) -> ( 1st ` ( ( i ` j ) ` l ) ) = ( 1st ` ( ( i ` j ) ` k ) ) )
142 id 
 |-  ( k e. X -> k e. X )
143 fvexd 
 |-  ( k e. X -> ( 1st ` ( ( i ` j ) ` k ) ) e. _V )
144 139 141 142 143 fvmptd 
 |-  ( k e. X -> ( ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) ` k ) = ( 1st ` ( ( i ` j ) ` k ) ) )
145 144 adantl 
 |-  ( ( n = j /\ k e. X ) -> ( ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) ` k ) = ( 1st ` ( ( i ` j ) ` k ) ) )
146 138 145 eqtrd 
 |-  ( ( n = j /\ k e. X ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) = ( 1st ` ( ( i ` j ) ` k ) ) )
147 134 fveq2d 
 |-  ( ( n = j /\ l e. X ) -> ( 2nd ` ( ( i ` n ) ` l ) ) = ( 2nd ` ( ( i ` j ) ` l ) ) )
148 147 mpteq2dva 
 |-  ( n = j -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) = ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) )
149 148 fveq1d 
 |-  ( n = j -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) = ( ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) ` k ) )
150 149 adantr 
 |-  ( ( n = j /\ k e. X ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) = ( ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) ` k ) )
151 eqidd 
 |-  ( k e. X -> ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) = ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) )
152 2fveq3 
 |-  ( l = k -> ( 2nd ` ( ( i ` j ) ` l ) ) = ( 2nd ` ( ( i ` j ) ` k ) ) )
153 152 adantl 
 |-  ( ( k e. X /\ l = k ) -> ( 2nd ` ( ( i ` j ) ` l ) ) = ( 2nd ` ( ( i ` j ) ` k ) ) )
154 fvexd 
 |-  ( k e. X -> ( 2nd ` ( ( i ` j ) ` k ) ) e. _V )
155 151 153 142 154 fvmptd 
 |-  ( k e. X -> ( ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) ` k ) = ( 2nd ` ( ( i ` j ) ` k ) ) )
156 155 adantl 
 |-  ( ( n = j /\ k e. X ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) ` k ) = ( 2nd ` ( ( i ` j ) ` k ) ) )
157 150 156 eqtrd 
 |-  ( ( n = j /\ k e. X ) -> ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) = ( 2nd ` ( ( i ` j ) ` k ) ) )
158 146 157 oveq12d 
 |-  ( ( n = j /\ k e. X ) -> ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) = ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) )
159 158 fveq2d 
 |-  ( ( n = j /\ k e. X ) -> ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) = ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) )
160 159 prodeq2dv 
 |-  ( n = j -> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) = prod_ k e. X ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) )
161 160 cbvmptv 
 |-  ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) )
162 161 a1i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) ) )
163 78 eqcomd 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) /\ k e. X ) -> ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) = ( ( [,) o. ( i ` j ) ) ` k ) )
164 163 fveq2d 
 |-  ( ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) = ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
165 164 prodeq2dv 
 |-  ( ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
166 165 mpteq2dva 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( 1st ` ( ( i ` j ) ` k ) ) [,) ( 2nd ` ( ( i ` j ) ` k ) ) ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
167 162 166 eqtrd 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
168 167 fveq2d 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( sum^ ` ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
169 168 3ad2ant2 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
170 92 adantll 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( ( F ` i ) ` n ) = ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
171 112 adantll 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( ( S ` i ) ` n ) = ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
172 170 171 oveq12d 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) = ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ( L ` X ) ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )
173 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> X e. Fin )
174 2 ad2antrr 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> X =/= (/) )
175 23 adantlll 
 |-  ( ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) /\ l e. X ) -> ( ( i ` n ) ` l ) e. ( RR X. RR ) )
176 175 24 syl 
 |-  ( ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) /\ l e. X ) -> ( 1st ` ( ( i ` n ) ` l ) ) e. RR )
177 176 fmpttd 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) : X --> RR )
178 175 49 syl 
 |-  ( ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) /\ l e. X ) -> ( 2nd ` ( ( i ` n ) ` l ) ) e. RR )
179 178 fmpttd 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) : X --> RR )
180 6 173 174 177 179 hoidmvn0val 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ( L ` X ) ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) = prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) )
181 172 180 eqtrd 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ n e. NN ) -> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) = prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) )
182 181 mpteq2dva 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) -> ( n e. NN |-> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) ) = ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) )
183 182 fveq2d 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) -> ( sum^ ` ( n e. NN |-> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) ) ) = ( sum^ ` ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) ) )
184 183 3adant3 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( n e. NN |-> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) ) ) = ( sum^ ` ( n e. NN |-> prod_ k e. X ( vol ` ( ( ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ` k ) [,) ( ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ` k ) ) ) ) ) )
185 simp3 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
186 169 184 185 3eqtr4d 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( n e. NN |-> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) ) ) = z )
187 186 3adant3l 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( sum^ ` ( n e. NN |-> ( ( ( F ` i ) ` n ) ( L ` X ) ( ( S ` i ) ` n ) ) ) ) = z )
188 131 187 breqtrd 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( A ( L ` X ) B ) <_ z )
189 188 3exp 
 |-  ( ph -> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( A ( L ` X ) B ) <_ z ) ) )
190 189 adantr 
 |-  ( ( ph /\ z e. M ) -> ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> ( ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( A ( L ` X ) B ) <_ z ) ) )
191 190 rexlimdv 
 |-  ( ( ph /\ z e. M ) -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( A ( L ` X ) B ) <_ z ) )
192 15 191 mpd 
 |-  ( ( ph /\ z e. M ) -> ( A ( L ` X ) B ) <_ z )
193 192 ralrimiva 
 |-  ( ph -> A. z e. M ( A ( L ` X ) B ) <_ z )
194 ssrab2 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR*
195 7 194 eqsstri 
 |-  M C_ RR*
196 195 a1i 
 |-  ( ph -> M C_ RR* )
197 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
198 6 1 3 4 hoidmvcl 
 |-  ( ph -> ( A ( L ` X ) B ) e. ( 0 [,) +oo ) )
199 197 198 sseldi 
 |-  ( ph -> ( A ( L ` X ) B ) e. RR* )
200 infxrgelb 
 |-  ( ( M C_ RR* /\ ( A ( L ` X ) B ) e. RR* ) -> ( ( A ( L ` X ) B ) <_ inf ( M , RR* , < ) <-> A. z e. M ( A ( L ` X ) B ) <_ z ) )
201 196 199 200 syl2anc 
 |-  ( ph -> ( ( A ( L ` X ) B ) <_ inf ( M , RR* , < ) <-> A. z e. M ( A ( L ` X ) B ) <_ z ) )
202 193 201 mpbird 
 |-  ( ph -> ( A ( L ` X ) B ) <_ inf ( M , RR* , < ) )
203 5 a1i 
 |-  ( ph -> I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
204 nfv 
 |-  F/ k ph
205 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
206 4 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
207 206 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
208 204 205 207 hoissrrn2 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ ( RR ^m X ) )
209 203 208 eqsstrd 
 |-  ( ph -> I C_ ( RR ^m X ) )
210 1 2 209 7 ovnn0val 
 |-  ( ph -> ( ( voln* ` X ) ` I ) = inf ( M , RR* , < ) )
211 210 eqcomd 
 |-  ( ph -> inf ( M , RR* , < ) = ( ( voln* ` X ) ` I ) )
212 202 211 breqtrd 
 |-  ( ph -> ( A ( L ` X ) B ) <_ ( ( voln* ` X ) ` I ) )