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