Metamath Proof Explorer

Theorem vonioo

Description: The n-dimensional Lebesgue measure of an open interval. This is the first statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 vonioo.x 
 |-  ( ph -> X e. Fin )
2 vonioo.a 
 |-  ( ph -> A : X --> RR )
3 vonioo.b 
 |-  ( ph -> B : X --> RR )
4 vonioo.i 
 |-  I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) )
5 vonioo.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 2 adantr 
 |-  ( ( ph /\ X = (/) ) -> A : X --> RR )
7 feq2 
 |-  ( X = (/) -> ( A : X --> RR <-> A : (/) --> RR ) )
8 7 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( A : X --> RR <-> A : (/) --> RR ) )
9 6 8 mpbid 
 |-  ( ( ph /\ X = (/) ) -> A : (/) --> RR )
10 3 adantr 
 |-  ( ( ph /\ X = (/) ) -> B : X --> RR )
11 feq2 
 |-  ( X = (/) -> ( B : X --> RR <-> B : (/) --> RR ) )
12 11 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( B : X --> RR <-> B : (/) --> RR ) )
13 10 12 mpbid 
 |-  ( ( ph /\ X = (/) ) -> B : (/) --> RR )
14 5 9 13 hoidmv0val 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` (/) ) B ) = 0 )
15 14 eqcomd 
 |-  ( ( ph /\ X = (/) ) -> 0 = ( A ( L ` (/) ) B ) )
16 fveq2 
 |-  ( X = (/) -> ( voln ` X ) = ( voln ` (/) ) )
17 4 a1i 
 |-  ( X = (/) -> I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
18 ixpeq1 
 |-  ( X = (/) -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) = X_ k e. (/) ( ( A ` k ) (,) ( B ` k ) ) )
19 17 18 eqtrd 
 |-  ( X = (/) -> I = X_ k e. (/) ( ( A ` k ) (,) ( B ` k ) ) )
20 16 19 fveq12d 
 |-  ( X = (/) -> ( ( voln ` X ) ` I ) = ( ( voln ` (/) ) ` X_ k e. (/) ( ( A ` k ) (,) ( B ` k ) ) ) )
21 20 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` I ) = ( ( voln ` (/) ) ` X_ k e. (/) ( ( A ` k ) (,) ( B ` k ) ) ) )
22 0fin 
 |-  (/) e. Fin
23 22 a1i 
 |-  ( ( ph /\ X = (/) ) -> (/) e. Fin )
24 eqid 
 |-  dom ( voln ` (/) ) = dom ( voln ` (/) )
25 ressxr 
 |-  RR C_ RR*
26 25 a1i 
 |-  ( ( ph /\ X = (/) ) -> RR C_ RR* )
27 9 26 fssd 
 |-  ( ( ph /\ X = (/) ) -> A : (/) --> RR* )
28 13 26 fssd 
 |-  ( ( ph /\ X = (/) ) -> B : (/) --> RR* )
29 23 24 27 28 ioovonmbl 
 |-  ( ( ph /\ X = (/) ) -> X_ k e. (/) ( ( A ` k ) (,) ( B ` k ) ) e. dom ( voln ` (/) ) )
30 29 von0val 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` (/) ) ` X_ k e. (/) ( ( A ` k ) (,) ( B ` k ) ) ) = 0 )
31 21 30 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` I ) = 0 )
32 fveq2 
 |-  ( X = (/) -> ( L ` X ) = ( L ` (/) ) )
33 32 oveqd 
 |-  ( X = (/) -> ( A ( L ` X ) B ) = ( A ( L ` (/) ) B ) )
34 33 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) B ) = ( A ( L ` (/) ) B ) )
35 15 31 34 3eqtr4d 
 |-  ( ( ph /\ X = (/) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
36 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
37 36 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
38 nfv 
 |-  F/ k ( ph /\ X =/= (/) )
39 nfra1 
 |-  F/ k A. k e. X ( A ` k ) < ( B ` k )
40 38 39 nfan 
 |-  F/ k ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) )
41 2 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
42 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
43 volico 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
44 41 42 43 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
45 44 ad4ant14 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
46 rspa 
 |-  ( ( A. k e. X ( A ` k ) < ( B ` k ) /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
47 46 iftrued 
 |-  ( ( A. k e. X ( A ` k ) < ( B ` k ) /\ k e. X ) -> if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) = ( ( B ` k ) - ( A ` k ) ) )
48 47 adantll 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) /\ k e. X ) -> if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) = ( ( B ` k ) - ( A ` k ) ) )
49 45 48 eqtrd 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) )
50 49 ex 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( k e. X -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) ) )
51 40 50 ralrimi 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> A. k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) )
52 51 prodeq2d 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
53 52 eqcomd 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> prod_ k e. X ( ( B ` k ) - ( A ` k ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
54 fveq2 
 |-  ( k = j -> ( A ` k ) = ( A ` j ) )
55 fveq2 
 |-  ( k = j -> ( B ` k ) = ( B ` j ) )
56 54 55 breq12d 
 |-  ( k = j -> ( ( A ` k ) < ( B ` k ) <-> ( A ` j ) < ( B ` j ) ) )
57 56 cbvralvw 
 |-  ( A. k e. X ( A ` k ) < ( B ` k ) <-> A. j e. X ( A ` j ) < ( B ` j ) )
58 57 biimpi 
 |-  ( A. k e. X ( A ` k ) < ( B ` k ) -> A. j e. X ( A ` j ) < ( B ` j ) )
59 58 adantl 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> A. j e. X ( A ` j ) < ( B ` j ) )
60 1 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X e. Fin )
61 60 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> X e. Fin )
62 2 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> A : X --> RR )
63 62 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> A : X --> RR )
64 3 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> B : X --> RR )
65 64 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> B : X --> RR )
66 simpr 
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
67 66 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> X =/= (/) )
68 57 46 sylanbr 
 |-  ( ( A. j e. X ( A ` j ) < ( B ` j ) /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
69 68 adantll 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
70 fveq2 
 |-  ( j = k -> ( A ` j ) = ( A ` k ) )
71 70 oveq1d 
 |-  ( j = k -> ( ( A ` j ) + ( 1 / m ) ) = ( ( A ` k ) + ( 1 / m ) ) )
72 71 cbvmptv 
 |-  ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) )
73 72 a1i 
 |-  ( m = n -> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) )
74 oveq2 
 |-  ( m = n -> ( 1 / m ) = ( 1 / n ) )
75 74 oveq2d 
 |-  ( m = n -> ( ( A ` k ) + ( 1 / m ) ) = ( ( A ` k ) + ( 1 / n ) ) )
76 75 mpteq2dv 
 |-  ( m = n -> ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
77 73 76 eqtrd 
 |-  ( m = n -> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
78 77 cbvmptv 
 |-  ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
79 nfcv 
 |-  F/_ n X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) ` k ) [,) ( B ` k ) )
80 nfcv 
 |-  F/_ m X
81 nffvmpt1 
 |-  F/_ m ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n )
82 nfcv 
 |-  F/_ m k
83 81 82 nffv 
 |-  F/_ m ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k )
84 nfcv 
 |-  F/_ m [,)
85 nfcv 
 |-  F/_ m ( B ` k )
86 83 84 85 nfov 
 |-  F/_ m ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) )
87 80 86 nfixpw 
 |-  F/_ m X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) )
88 fveq2 
 |-  ( m = n -> ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) = ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) )
89 88 fveq1d 
 |-  ( m = n -> ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) ` k ) = ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) )
90 89 oveq1d 
 |-  ( m = n -> ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) ` k ) [,) ( B ` k ) ) = ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) ) )
91 90 ixpeq2dv 
 |-  ( m = n -> X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) ) )
92 79 87 91 cbvmpt 
 |-  ( m e. NN |-> X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) ` k ) [,) ( B ` k ) ) ) = ( n e. NN |-> X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) ) )
93 61 63 65 67 69 4 78 92 vonioolem2 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
94 59 93 syldan 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
95 5 60 66 62 64 hoidmvn0val 
 |-  ( ( ph /\ X =/= (/) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
96 95 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
97 53 94 96 3eqtr4d 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
98 rexnal 
 |-  ( E. k e. X -. ( A ` k ) < ( B ` k ) <-> -. A. k e. X ( A ` k ) < ( B ` k ) )
99 98 bicomi 
 |-  ( -. A. k e. X ( A ` k ) < ( B ` k ) <-> E. k e. X -. ( A ` k ) < ( B ` k ) )
100 99 biimpi 
 |-  ( -. A. k e. X ( A ` k ) < ( B ` k ) -> E. k e. X -. ( A ` k ) < ( B ` k ) )
101 100 adantl 
 |-  ( ( ph /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> E. k e. X -. ( A ` k ) < ( B ` k ) )
102 simpr 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> -. ( A ` k ) < ( B ` k ) )
103 42 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( B ` k ) e. RR )
104 41 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( A ` k ) e. RR )
105 103 104 lenltd 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( ( B ` k ) <_ ( A ` k ) <-> -. ( A ` k ) < ( B ` k ) ) )
106 102 105 mpbird 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( B ` k ) <_ ( A ` k ) )
107 106 ex 
 |-  ( ( ph /\ k e. X ) -> ( -. ( A ` k ) < ( B ` k ) -> ( B ` k ) <_ ( A ` k ) ) )
108 107 reximdva 
 |-  ( ph -> ( E. k e. X -. ( A ` k ) < ( B ` k ) -> E. k e. X ( B ` k ) <_ ( A ` k ) ) )
109 108 adantr 
 |-  ( ( ph /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> ( E. k e. X -. ( A ` k ) < ( B ` k ) -> E. k e. X ( B ` k ) <_ ( A ` k ) ) )
110 101 109 mpd 
 |-  ( ( ph /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> E. k e. X ( B ` k ) <_ ( A ` k ) )
111 110 adantlr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> E. k e. X ( B ` k ) <_ ( A ` k ) )
112 nfcv 
 |-  F/_ k ( voln ` X )
113 nfixp1 
 |-  F/_ k X_ k e. X ( ( A ` k ) (,) ( B ` k ) )
114 4 113 nfcxfr 
 |-  F/_ k I
115 112 114 nffv 
 |-  F/_ k ( ( voln ` X ) ` I )
116 nfcv 
 |-  F/_ k ( A ( L ` X ) B )
117 115 116 nfeq 
 |-  F/ k ( ( voln ` X ) ` I ) = ( A ( L ` X ) B )
118 1 vonmea 
 |-  ( ph -> ( voln ` X ) e. Meas )
119 118 mea0 
 |-  ( ph -> ( ( voln ` X ) ` (/) ) = 0 )
120 119 3ad2ant1 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` (/) ) = 0 )
121 4 a1i 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
122 simp2 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> k e. X )
123 simp3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( B ` k ) <_ ( A ` k ) )
124 25 41 sseldi 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
125 124 3adant3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( A ` k ) e. RR* )
126 25 42 sseldi 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
127 126 3adant3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( B ` k ) e. RR* )
128 ioo0 
 |-  ( ( ( A ` k ) e. RR* /\ ( B ` k ) e. RR* ) -> ( ( ( A ` k ) (,) ( B ` k ) ) = (/) <-> ( B ` k ) <_ ( A ` k ) ) )
129 125 127 128 syl2anc 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( ( A ` k ) (,) ( B ` k ) ) = (/) <-> ( B ` k ) <_ ( A ` k ) ) )
130 123 129 mpbird 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( A ` k ) (,) ( B ` k ) ) = (/) )
131 rspe 
 |-  ( ( k e. X /\ ( ( A ` k ) (,) ( B ` k ) ) = (/) ) -> E. k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
132 122 130 131 syl2anc 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> E. k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
133 ixp0 
 |-  ( E. k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
134 132 133 syl 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
135 121 134 eqtrd 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> I = (/) )
136 135 fveq2d 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` I ) = ( ( voln ` X ) ` (/) ) )
137 ne0i 
 |-  ( k e. X -> X =/= (/) )
138 137 adantl 
 |-  ( ( ph /\ k e. X ) -> X =/= (/) )
139 138 95 syldan 
 |-  ( ( ph /\ k e. X ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
140 139 3adant3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
141 eleq1w 
 |-  ( j = k -> ( j e. X <-> k e. X ) )
142 fveq2 
 |-  ( j = k -> ( B ` j ) = ( B ` k ) )
143 142 70 breq12d 
 |-  ( j = k -> ( ( B ` j ) <_ ( A ` j ) <-> ( B ` k ) <_ ( A ` k ) ) )
144 141 143 3anbi23d 
 |-  ( j = k -> ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) <-> ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) ) )
145 144 imbi1d 
 |-  ( j = k -> ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 ) <-> ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 ) ) )
146 nfv 
 |-  F/ k ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) )
147 1 3ad2ant1 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> X e. Fin )
148 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
149 41 42 148 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
150 149 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
151 150 3ad2antl1 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
152 simp2 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> j e. X )
153 54 55 oveq12d 
 |-  ( k = j -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` j ) [,) ( B ` j ) ) )
154 153 fveq2d 
 |-  ( k = j -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) )
155 154 adantl 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k = j ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) )
156 2 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) e. RR )
157 3 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( B ` j ) e. RR )
158 volico 
 |-  ( ( ( A ` j ) e. RR /\ ( B ` j ) e. RR ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
159 156 157 158 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
160 159 3adant3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
161 simp3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( B ` j ) <_ ( A ` j ) )
162 157 156 lenltd 
 |-  ( ( ph /\ j e. X ) -> ( ( B ` j ) <_ ( A ` j ) <-> -. ( A ` j ) < ( B ` j ) ) )
163 162 3adant3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( ( B ` j ) <_ ( A ` j ) <-> -. ( A ` j ) < ( B ` j ) ) )
164 161 163 mpbid 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> -. ( A ` j ) < ( B ` j ) )
165 164 iffalsed 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) = 0 )
166 160 165 eqtrd 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = 0 )
167 166 adantr 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k = j ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = 0 )
168 155 167 eqtrd 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k = j ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
169 146 147 151 152 168 fprodeq0g 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
170 145 169 chvarvv 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
171 140 170 eqtrd 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( A ( L ` X ) B ) = 0 )
172 120 136 171 3eqtr4d 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
173 172 3exp 
 |-  ( ph -> ( k e. X -> ( ( B ` k ) <_ ( A ` k ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) ) )
174 173 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( k e. X -> ( ( B ` k ) <_ ( A ` k ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) ) )
175 38 117 174 rexlimd 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. k e. X ( B ` k ) <_ ( A ` k ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) )
176 175 imp 
 |-  ( ( ( ph /\ X =/= (/) ) /\ E. k e. X ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
177 111 176 syldan 
 |-  ( ( ( ph /\ X =/= (/) ) /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
178 97 177 pm2.61dan 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
179 37 178 syldan 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
180 35 179 pm2.61dan 
 |-  ( ph -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )