Metamath Proof Explorer

Theorem ovnhoi

Description: The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoi.x 
|- ( ph -> X e. Fin )
ovnhoi.a 
|- ( ph -> A : X --> RR )
ovnhoi.b 
|- ( ph -> B : X --> RR )
ovnhoi.c 
|- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
ovnhoi.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 ) ) ) ) ) )
Assertion ovnhoi 
|- ( ph -> ( ( voln* ` X ) ` I ) = ( A ( L ` X ) B ) )

Proof

Step Hyp Ref Expression
1 ovnhoi.x 
 |-  ( ph -> X e. Fin )
2 ovnhoi.a 
 |-  ( ph -> A : X --> RR )
3 ovnhoi.b 
 |-  ( ph -> B : X --> RR )
4 ovnhoi.c 
 |-  I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
5 ovnhoi.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 ) ) ) ) ) )
6 4 a1i 
 |-  ( ph -> I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
7 nfv 
 |-  F/ k ph
8 2 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
9 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
10 9 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
11 7 8 10 hoissrrn2 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ ( RR ^m X ) )
12 6 11 eqsstrd 
 |-  ( ph -> I C_ ( RR ^m X ) )
13 1 12 ovnxrcl 
 |-  ( ph -> ( ( voln* ` X ) ` I ) e. RR* )
14 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
15 5 1 2 3 hoidmvcl 
 |-  ( ph -> ( A ( L ` X ) B ) e. ( 0 [,) +oo ) )
16 14 15 sselid 
 |-  ( ph -> ( A ( L ` X ) B ) e. RR* )
17 fveq2 
 |-  ( X = (/) -> ( voln* ` X ) = ( voln* ` (/) ) )
18 17 fveq1d 
 |-  ( X = (/) -> ( ( voln* ` X ) ` I ) = ( ( voln* ` (/) ) ` I ) )
19 18 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` I ) = ( ( voln* ` (/) ) ` I ) )
20 ixpeq1 
 |-  ( X = (/) -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) = X_ k e. (/) ( ( A ` k ) [,) ( B ` k ) ) )
21 ixp0x 
 |-  X_ k e. (/) ( ( A ` k ) [,) ( B ` k ) ) = { (/) }
22 21 a1i 
 |-  ( X = (/) -> X_ k e. (/) ( ( A ` k ) [,) ( B ` k ) ) = { (/) } )
23 20 22 eqtrd 
 |-  ( X = (/) -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) = { (/) } )
24 23 adantl 
 |-  ( ( ph /\ X = (/) ) -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) = { (/) } )
25 4 a1i 
 |-  ( ( ph /\ X = (/) ) -> I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
26 reex 
 |-  RR e. _V
27 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
28 26 27 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
29 28 a1i 
 |-  ( ( ph /\ X = (/) ) -> ( RR ^m (/) ) = { (/) } )
30 24 25 29 3eqtr4d 
 |-  ( ( ph /\ X = (/) ) -> I = ( RR ^m (/) ) )
31 eqimss 
 |-  ( I = ( RR ^m (/) ) -> I C_ ( RR ^m (/) ) )
32 30 31 syl 
 |-  ( ( ph /\ X = (/) ) -> I C_ ( RR ^m (/) ) )
33 32 ovn0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` (/) ) ` I ) = 0 )
34 19 33 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` I ) = 0 )
35 0red 
 |-  ( ( ph /\ X = (/) ) -> 0 e. RR )
36 34 35 eqeltrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` I ) e. RR )
37 eqidd 
 |-  ( ( ph /\ X = (/) ) -> 0 = 0 )
38 fveq2 
 |-  ( X = (/) -> ( L ` X ) = ( L ` (/) ) )
39 38 oveqd 
 |-  ( X = (/) -> ( A ( L ` X ) B ) = ( A ( L ` (/) ) B ) )
40 39 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) B ) = ( A ( L ` (/) ) B ) )
41 2 adantr 
 |-  ( ( ph /\ X = (/) ) -> A : X --> RR )
42 simpr 
 |-  ( ( ph /\ X = (/) ) -> X = (/) )
43 42 feq2d 
 |-  ( ( ph /\ X = (/) ) -> ( A : X --> RR <-> A : (/) --> RR ) )
44 41 43 mpbid 
 |-  ( ( ph /\ X = (/) ) -> A : (/) --> RR )
45 3 adantr 
 |-  ( ( ph /\ X = (/) ) -> B : X --> RR )
46 42 feq2d 
 |-  ( ( ph /\ X = (/) ) -> ( B : X --> RR <-> B : (/) --> RR ) )
47 45 46 mpbid 
 |-  ( ( ph /\ X = (/) ) -> B : (/) --> RR )
48 5 44 47 hoidmv0val 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` (/) ) B ) = 0 )
49 40 48 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) B ) = 0 )
50 37 34 49 3eqtr4d 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` I ) = ( A ( L ` X ) B ) )
51 36 50 eqled 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln* ` X ) ` I ) <_ ( A ( L ` X ) B ) )
52 eqid 
 |-  { 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 ) ) ) ) ) }
53 eqeq1 
 |-  ( n = j -> ( n = 1 <-> j = 1 ) )
54 53 ifbid 
 |-  ( n = j -> if ( n = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) = if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) )
55 54 mpteq2dv 
 |-  ( n = j -> ( k e. X |-> if ( n = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) = ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
56 55 cbvmptv 
 |-  ( n e. NN |-> ( k e. X |-> if ( n = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) ) = ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
57 1 2 3 4 52 56 ovnhoilem1 
 |-  ( ph -> ( ( voln* ` X ) ` I ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
58 57 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` I ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
59 1 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
60 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
61 60 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
62 2 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> A : X --> RR )
63 3 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> B : X --> RR )
64 5 59 61 62 63 hoidmvn0val 
 |-  ( ( ph /\ -. X = (/) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
65 64 eqcomd 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( A ( L ` X ) B ) )
66 58 65 breqtrd 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln* ` X ) ` I ) <_ ( A ( L ` X ) B ) )
67 51 66 pm2.61dan 
 |-  ( ph -> ( ( voln* ` X ) ` I ) <_ ( A ( L ` X ) B ) )
68 49 35 eqeltrd 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) B ) e. RR )
69 50 eqcomd 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) B ) = ( ( voln* ` X ) ` I ) )
70 68 69 eqled 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) B ) <_ ( ( voln* ` X ) ` I ) )
71 fveq1 
 |-  ( a = c -> ( a ` k ) = ( c ` k ) )
72 71 fvoveq1d 
 |-  ( a = c -> ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( c ` k ) [,) ( b ` k ) ) ) )
73 72 prodeq2ad 
 |-  ( a = c -> prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. x ( vol ` ( ( c ` k ) [,) ( b ` k ) ) ) )
74 73 ifeq2d 
 |-  ( a = c -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( b ` k ) ) ) ) )
75 fveq1 
 |-  ( b = d -> ( b ` k ) = ( d ` k ) )
76 75 oveq2d 
 |-  ( b = d -> ( ( c ` k ) [,) ( b ` k ) ) = ( ( c ` k ) [,) ( d ` k ) ) )
77 76 fveq2d 
 |-  ( b = d -> ( vol ` ( ( c ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) )
78 77 prodeq2ad 
 |-  ( b = d -> prod_ k e. x ( vol ` ( ( c ` k ) [,) ( b ` k ) ) ) = prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) )
79 78 ifeq2d 
 |-  ( b = d -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) )
80 74 79 cbvmpov 
 |-  ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( c e. ( RR ^m x ) , d e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) )
81 80 a1i 
 |-  ( x = y -> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( c e. ( RR ^m x ) , d e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) ) )
82 oveq2 
 |-  ( x = y -> ( RR ^m x ) = ( RR ^m y ) )
83 eqeq1 
 |-  ( x = y -> ( x = (/) <-> y = (/) ) )
84 prodeq1 
 |-  ( x = y -> prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) = prod_ k e. y ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) )
85 83 84 ifbieq2d 
 |-  ( x = y -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) = if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) )
86 82 82 85 mpoeq123dv 
 |-  ( x = y -> ( c e. ( RR ^m x ) , d e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) ) = ( c e. ( RR ^m y ) , d e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) ) )
87 81 86 eqtrd 
 |-  ( x = y -> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( c e. ( RR ^m y ) , d e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) ) )
88 87 cbvmptv 
 |-  ( 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 ) ) ) ) ) ) = ( y e. Fin |-> ( c e. ( RR ^m y ) , d e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) ) )
89 5 88 eqtri 
 |-  L = ( y e. Fin |-> ( c e. ( RR ^m y ) , d e. ( RR ^m y ) |-> if ( y = (/) , 0 , prod_ k e. y ( vol ` ( ( c ` k ) [,) ( d ` k ) ) ) ) ) )
90 eqeq1 
 |-  ( w = z -> ( w = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) <-> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) )
91 90 anbi2d 
 |-  ( w = z -> ( ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ w = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) <-> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) ) )
92 91 rexbidv 
 |-  ( w = z -> ( E. h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ w = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) <-> E. h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) ) )
93 simpl 
 |-  ( ( h = i /\ j e. NN ) -> h = i )
94 93 fveq1d 
 |-  ( ( h = i /\ j e. NN ) -> ( h ` j ) = ( i ` j ) )
95 94 coeq2d 
 |-  ( ( h = i /\ j e. NN ) -> ( [,) o. ( h ` j ) ) = ( [,) o. ( i ` j ) ) )
96 95 fveq1d 
 |-  ( ( h = i /\ j e. NN ) -> ( ( [,) o. ( h ` j ) ) ` k ) = ( ( [,) o. ( i ` j ) ) ` k ) )
97 96 ixpeq2dv 
 |-  ( ( h = i /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
98 97 iuneq2dv 
 |-  ( h = i -> U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
99 98 sseq2d 
 |-  ( h = i -> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) <-> I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) )
100 simpl 
 |-  ( ( h = i /\ k e. X ) -> h = i )
101 100 fveq1d 
 |-  ( ( h = i /\ k e. X ) -> ( h ` j ) = ( i ` j ) )
102 101 coeq2d 
 |-  ( ( h = i /\ k e. X ) -> ( [,) o. ( h ` j ) ) = ( [,) o. ( i ` j ) ) )
103 102 fveq1d 
 |-  ( ( h = i /\ k e. X ) -> ( ( [,) o. ( h ` j ) ) ` k ) = ( ( [,) o. ( i ` j ) ) ` k ) )
104 103 fveq2d 
 |-  ( ( h = i /\ k e. X ) -> ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
105 104 prodeq2dv 
 |-  ( h = i -> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
106 105 mpteq2dv 
 |-  ( h = i -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) )
107 106 fveq2d 
 |-  ( h = i -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
108 107 eqeq2d 
 |-  ( h = i -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) <-> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
109 99 108 anbi12d 
 |-  ( h = i -> ( ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
110 109 cbvrexvw 
 |-  ( E. h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) <-> 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 ) ) ) ) ) )
111 110 a1i 
 |-  ( w = z -> ( E. h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
112 92 111 bitrd 
 |-  ( w = z -> ( E. h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ w = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` j ) ) ` k ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
113 112 cbvrabv 
 |-  { w e. RR* | E. h e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( h ` j ) ) ` k ) /\ w = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( h ` 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 ) ) ) ) ) }
114 simpl 
 |-  ( ( j = n /\ l e. X ) -> j = n )
115 114 fveq2d 
 |-  ( ( j = n /\ l e. X ) -> ( i ` j ) = ( i ` n ) )
116 115 fveq1d 
 |-  ( ( j = n /\ l e. X ) -> ( ( i ` j ) ` l ) = ( ( i ` n ) ` l ) )
117 116 fveq2d 
 |-  ( ( j = n /\ l e. X ) -> ( 1st ` ( ( i ` j ) ` l ) ) = ( 1st ` ( ( i ` n ) ` l ) ) )
118 117 mpteq2dva 
 |-  ( j = n -> ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) = ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
119 118 cbvmptv 
 |-  ( j e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) ) = ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) )
120 119 mpteq2i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( j e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` j ) ` l ) ) ) ) ) = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )
121 116 fveq2d 
 |-  ( ( j = n /\ l e. X ) -> ( 2nd ` ( ( i ` j ) ` l ) ) = ( 2nd ` ( ( i ` n ) ` l ) ) )
122 121 mpteq2dva 
 |-  ( j = n -> ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) = ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
123 122 cbvmptv 
 |-  ( j e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) ) = ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) )
124 123 mpteq2i 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( j e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` j ) ` l ) ) ) ) ) = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )
125 59 61 62 63 4 89 113 120 124 ovnhoilem2 
 |-  ( ( ph /\ -. X = (/) ) -> ( A ( L ` X ) B ) <_ ( ( voln* ` X ) ` I ) )
126 70 125 pm2.61dan 
 |-  ( ph -> ( A ( L ` X ) B ) <_ ( ( voln* ` X ) ` I ) )
127 13 16 67 126 xrletrid 
 |-  ( ph -> ( ( voln* ` X ) ` I ) = ( A ( L ` X ) B ) )