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 0fi 
 |-  (/) 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 ffvelcdmda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
42 3 ffvelcdmda 
 |-  ( ( 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 bilani 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> A. j e. X ( A ` j ) < ( B ` j ) )
59 1 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X e. Fin )
60 59 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> X e. Fin )
61 2 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> A : X --> RR )
62 61 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> A : X --> RR )
63 3 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> B : X --> RR )
64 63 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> B : X --> RR )
65 simpr 
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
66 65 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> X =/= (/) )
67 57 46 sylanbr 
 |-  ( ( A. j e. X ( A ` j ) < ( B ` j ) /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
68 67 adantll 
 |-  ( ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) /\ k e. X ) -> ( A ` k ) < ( B ` k ) )
69 fveq2 
 |-  ( j = k -> ( A ` j ) = ( A ` k ) )
70 69 oveq1d 
 |-  ( j = k -> ( ( A ` j ) + ( 1 / m ) ) = ( ( A ` k ) + ( 1 / m ) ) )
71 70 cbvmptv 
 |-  ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) )
72 71 a1i 
 |-  ( m = n -> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) )
73 oveq2 
 |-  ( m = n -> ( 1 / m ) = ( 1 / n ) )
74 73 oveq2d 
 |-  ( m = n -> ( ( A ` k ) + ( 1 / m ) ) = ( ( A ` k ) + ( 1 / n ) ) )
75 74 mpteq2dv 
 |-  ( m = n -> ( k e. X |-> ( ( A ` k ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
76 72 75 eqtrd 
 |-  ( m = n -> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) = ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
77 76 cbvmptv 
 |-  ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) = ( n e. NN |-> ( k e. X |-> ( ( A ` k ) + ( 1 / n ) ) ) )
78 nfcv 
 |-  F/_ n X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` m ) ` k ) [,) ( B ` k ) )
79 nfcv 
 |-  F/_ m X
80 nffvmpt1 
 |-  F/_ m ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n )
81 nfcv 
 |-  F/_ m k
82 80 81 nffv 
 |-  F/_ m ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k )
83 nfcv 
 |-  F/_ m [,)
84 nfcv 
 |-  F/_ m ( B ` k )
85 82 83 84 nfov 
 |-  F/_ m ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) )
86 79 85 nfixpw 
 |-  F/_ m X_ k e. X ( ( ( ( m e. NN |-> ( j e. X |-> ( ( A ` j ) + ( 1 / m ) ) ) ) ` n ) ` k ) [,) ( B ` k ) )
87 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 ) )
88 87 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 ) )
89 88 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 ) ) )
90 89 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 ) ) )
91 78 86 90 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 ) ) )
92 60 62 64 66 68 4 77 91 vonioolem2 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. j e. X ( A ` j ) < ( B ` j ) ) -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
93 58 92 syldan 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( ( voln ` X ) ` I ) = prod_ k e. X ( ( B ` k ) - ( A ` k ) ) )
94 5 59 65 61 63 hoidmvn0val 
 |-  ( ( ph /\ X =/= (/) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
95 94 adantr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
96 53 93 95 3eqtr4d 
 |-  ( ( ( ph /\ X =/= (/) ) /\ A. k e. X ( A ` k ) < ( B ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
97 rexnal 
 |-  ( E. k e. X -. ( A ` k ) < ( B ` k ) <-> -. A. k e. X ( A ` k ) < ( B ` k ) )
98 97 bilanri 
 |-  ( ( ph /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> E. k e. X -. ( A ` k ) < ( B ` k ) )
99 simpr 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> -. ( A ` k ) < ( B ` k ) )
100 42 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( B ` k ) e. RR )
101 41 adantr 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( A ` k ) e. RR )
102 100 101 lenltd 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( ( B ` k ) <_ ( A ` k ) <-> -. ( A ` k ) < ( B ` k ) ) )
103 99 102 mpbird 
 |-  ( ( ( ph /\ k e. X ) /\ -. ( A ` k ) < ( B ` k ) ) -> ( B ` k ) <_ ( A ` k ) )
104 103 ex 
 |-  ( ( ph /\ k e. X ) -> ( -. ( A ` k ) < ( B ` k ) -> ( B ` k ) <_ ( A ` k ) ) )
105 104 reximdva 
 |-  ( ph -> ( E. k e. X -. ( A ` k ) < ( B ` k ) -> E. k e. X ( B ` k ) <_ ( A ` k ) ) )
106 105 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 ) ) )
107 98 106 mpd 
 |-  ( ( ph /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> E. k e. X ( B ` k ) <_ ( A ` k ) )
108 107 adantlr 
 |-  ( ( ( ph /\ X =/= (/) ) /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> E. k e. X ( B ` k ) <_ ( A ` k ) )
109 nfcv 
 |-  F/_ k ( voln ` X )
110 nfixp1 
 |-  F/_ k X_ k e. X ( ( A ` k ) (,) ( B ` k ) )
111 4 110 nfcxfr 
 |-  F/_ k I
112 109 111 nffv 
 |-  F/_ k ( ( voln ` X ) ` I )
113 nfcv 
 |-  F/_ k ( A ( L ` X ) B )
114 112 113 nfeq 
 |-  F/ k ( ( voln ` X ) ` I ) = ( A ( L ` X ) B )
115 1 vonmea 
 |-  ( ph -> ( voln ` X ) e. Meas )
116 115 mea0 
 |-  ( ph -> ( ( voln ` X ) ` (/) ) = 0 )
117 116 3ad2ant1 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` (/) ) = 0 )
118 4 a1i 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> I = X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) )
119 simp2 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> k e. X )
120 simp3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( B ` k ) <_ ( A ` k ) )
121 25 41 sselid 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR* )
122 121 3adant3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( A ` k ) e. RR* )
123 25 42 sselid 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
124 123 3adant3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( B ` k ) e. RR* )
125 ioo0 
 |-  ( ( ( A ` k ) e. RR* /\ ( B ` k ) e. RR* ) -> ( ( ( A ` k ) (,) ( B ` k ) ) = (/) <-> ( B ` k ) <_ ( A ` k ) ) )
126 122 124 125 syl2anc 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( ( A ` k ) (,) ( B ` k ) ) = (/) <-> ( B ` k ) <_ ( A ` k ) ) )
127 120 126 mpbird 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( A ` k ) (,) ( B ` k ) ) = (/) )
128 rspe 
 |-  ( ( k e. X /\ ( ( A ` k ) (,) ( B ` k ) ) = (/) ) -> E. k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
129 119 127 128 syl2anc 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> E. k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
130 ixp0 
 |-  ( E. k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
131 129 130 syl 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> X_ k e. X ( ( A ` k ) (,) ( B ` k ) ) = (/) )
132 118 131 eqtrd 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> I = (/) )
133 132 fveq2d 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` I ) = ( ( voln ` X ) ` (/) ) )
134 ne0i 
 |-  ( k e. X -> X =/= (/) )
135 134 adantl 
 |-  ( ( ph /\ k e. X ) -> X =/= (/) )
136 135 94 syldan 
 |-  ( ( ph /\ k e. X ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
137 136 3adant3 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
138 eleq1w 
 |-  ( j = k -> ( j e. X <-> k e. X ) )
139 fveq2 
 |-  ( j = k -> ( B ` j ) = ( B ` k ) )
140 139 69 breq12d 
 |-  ( j = k -> ( ( B ` j ) <_ ( A ` j ) <-> ( B ` k ) <_ ( A ` k ) ) )
141 138 140 3anbi23d 
 |-  ( j = k -> ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) <-> ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) ) )
142 141 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 ) ) )
143 nfv 
 |-  F/ k ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) )
144 1 3ad2ant1 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> X e. Fin )
145 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
146 41 42 145 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
147 146 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
148 147 3ad2antl1 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
149 simp2 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> j e. X )
150 54 55 oveq12d 
 |-  ( k = j -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` j ) [,) ( B ` j ) ) )
151 150 fveq2d 
 |-  ( k = j -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) )
152 151 adantl 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k = j ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) )
153 2 ffvelcdmda 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) e. RR )
154 3 ffvelcdmda 
 |-  ( ( ph /\ j e. X ) -> ( B ` j ) e. RR )
155 volico 
 |-  ( ( ( A ` j ) e. RR /\ ( B ` j ) e. RR ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
156 153 154 155 syl2anc 
 |-  ( ( ph /\ j e. X ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
157 156 3adant3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
158 simp3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( B ` j ) <_ ( A ` j ) )
159 154 153 lenltd 
 |-  ( ( ph /\ j e. X ) -> ( ( B ` j ) <_ ( A ` j ) <-> -. ( A ` j ) < ( B ` j ) ) )
160 159 3adant3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( ( B ` j ) <_ ( A ` j ) <-> -. ( A ` j ) < ( B ` j ) ) )
161 158 160 mpbid 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> -. ( A ` j ) < ( B ` j ) )
162 161 iffalsed 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) = 0 )
163 157 162 eqtrd 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = 0 )
164 163 adantr 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k = j ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = 0 )
165 152 164 eqtrd 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k = j ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
166 143 144 148 149 165 fprodeq0g 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
167 142 166 chvarvv 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
168 137 167 eqtrd 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( A ( L ` X ) B ) = 0 )
169 117 133 168 3eqtr4d 
 |-  ( ( ph /\ k e. X /\ ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
170 169 3exp 
 |-  ( ph -> ( k e. X -> ( ( B ` k ) <_ ( A ` k ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) ) )
171 170 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( k e. X -> ( ( B ` k ) <_ ( A ` k ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) ) )
172 38 114 171 rexlimd 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. k e. X ( B ` k ) <_ ( A ` k ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) ) )
173 172 imp 
 |-  ( ( ( ph /\ X =/= (/) ) /\ E. k e. X ( B ` k ) <_ ( A ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
174 108 173 syldan 
 |-  ( ( ( ph /\ X =/= (/) ) /\ -. A. k e. X ( A ` k ) < ( B ` k ) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
175 96 174 pm2.61dan 
 |-  ( ( ph /\ X =/= (/) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
176 37 175 syldan 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )
177 35 176 pm2.61dan 
 |-  ( ph -> ( ( voln ` X ) ` I ) = ( A ( L ` X ) B ) )