Metamath Proof Explorer

Theorem vonicc

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

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

Proof

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