Metamath Proof Explorer

Theorem hoidmv1le

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of Fremlin1 p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1le.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 ) ) ) ) ) )
hoidmv1le.z 
|- ( ph -> Z e. V )
hoidmv1le.x 
|- X = { Z }
hoidmv1le.a 
|- ( ph -> A : X --> RR )
hoidmv1le.b 
|- ( ph -> B : X --> RR )
hoidmv1le.c 
|- ( ph -> C : NN --> ( RR ^m X ) )
hoidmv1le.d 
|- ( ph -> D : NN --> ( RR ^m X ) )
hoidmv1le.s 
|- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
Assertion hoidmv1le 
|- ( ph -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmv1le.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 ) ) ) ) ) )
2 hoidmv1le.z 
 |-  ( ph -> Z e. V )
3 hoidmv1le.x 
 |-  X = { Z }
4 hoidmv1le.a 
 |-  ( ph -> A : X --> RR )
5 hoidmv1le.b 
 |-  ( ph -> B : X --> RR )
6 hoidmv1le.c 
 |-  ( ph -> C : NN --> ( RR ^m X ) )
7 hoidmv1le.d 
 |-  ( ph -> D : NN --> ( RR ^m X ) )
8 hoidmv1le.s 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
9 snidg 
 |-  ( Z e. V -> Z e. { Z } )
10 2 9 syl 
 |-  ( ph -> Z e. { Z } )
11 10 3 eleqtrrdi 
 |-  ( ph -> Z e. X )
12 5 11 ffvelcdmd 
 |-  ( ph -> ( B ` Z ) e. RR )
13 4 11 ffvelcdmd 
 |-  ( ph -> ( A ` Z ) e. RR )
14 12 13 resubcld 
 |-  ( ph -> ( ( B ` Z ) - ( A ` Z ) ) e. RR )
15 14 rexrd 
 |-  ( ph -> ( ( B ` Z ) - ( A ` Z ) ) e. RR* )
16 pnfxr 
 |-  +oo e. RR*
17 16 a1i 
 |-  ( ph -> +oo e. RR* )
18 14 ltpnfd 
 |-  ( ph -> ( ( B ` Z ) - ( A ` Z ) ) < +oo )
19 15 17 18 xrltled 
 |-  ( ph -> ( ( B ` Z ) - ( A ` Z ) ) <_ +oo )
20 19 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( ( B ` Z ) - ( A ` Z ) ) <_ +oo )
21 id 
 |-  ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo )
22 21 eqcomd 
 |-  ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo -> +oo = ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> +oo = ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
24 20 23 breqtrd 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( ( B ` Z ) - ( A ` Z ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
25 simpl 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( ph /\ ( A ` Z ) < ( B ` Z ) ) )
26 simpr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo )
27 nnex 
 |-  NN e. _V
28 27 a1i 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> NN e. _V )
29 3 a1i 
 |-  ( ph -> X = { Z } )
30 snfi 
 |-  { Z } e. Fin
31 30 a1i 
 |-  ( ph -> { Z } e. Fin )
32 29 31 eqeltrd 
 |-  ( ph -> X e. Fin )
33 32 adantr 
 |-  ( ( ph /\ j e. NN ) -> X e. Fin )
34 11 ne0d 
 |-  ( ph -> X =/= (/) )
35 34 adantr 
 |-  ( ( ph /\ j e. NN ) -> X =/= (/) )
36 6 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m X ) )
37 elmapi 
 |-  ( ( C ` j ) e. ( RR ^m X ) -> ( C ` j ) : X --> RR )
38 36 37 syl 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) : X --> RR )
39 7 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m X ) )
40 elmapi 
 |-  ( ( D ` j ) e. ( RR ^m X ) -> ( D ` j ) : X --> RR )
41 39 40 syl 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) : X --> RR )
42 1 33 35 38 41 hoidmvn0val 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) = prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
43 3 prodeq1i 
 |-  prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = prod_ k e. { Z } ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
44 43 a1i 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = prod_ k e. { Z } ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
45 2 adantr 
 |-  ( ( ph /\ j e. NN ) -> Z e. V )
46 11 adantr 
 |-  ( ( ph /\ j e. NN ) -> Z e. X )
47 38 46 ffvelcdmd 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR )
48 41 46 ffvelcdmd 
 |-  ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR )
49 volicore 
 |-  ( ( ( ( C ` j ) ` Z ) e. RR /\ ( ( D ` j ) ` Z ) e. RR ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) e. RR )
50 47 48 49 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) e. RR )
51 50 recnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) e. CC )
52 fveq2 
 |-  ( k = Z -> ( ( C ` j ) ` k ) = ( ( C ` j ) ` Z ) )
53 fveq2 
 |-  ( k = Z -> ( ( D ` j ) ` k ) = ( ( D ` j ) ` Z ) )
54 52 53 oveq12d 
 |-  ( k = Z -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
55 54 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
56 55 prodsn 
 |-  ( ( Z e. V /\ ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) e. CC ) -> prod_ k e. { Z } ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
57 45 51 56 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. { Z } ( vol ` ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
58 42 44 57 3eqtrd 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
59 58 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) = ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) )
60 fveq2 
 |-  ( k = l -> ( a ` k ) = ( a ` l ) )
61 fveq2 
 |-  ( k = l -> ( b ` k ) = ( b ` l ) )
62 60 61 oveq12d 
 |-  ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) )
63 62 fveq2d 
 |-  ( k = l -> ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) )
64 63 cbvprodv 
 |-  prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) )
65 ifeq2 
 |-  ( prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) ) )
66 64 65 ax-mp 
 |-  if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) )
67 66 a1i 
 |-  ( ( a e. ( RR ^m x ) /\ b e. ( RR ^m x ) ) -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) ) )
68 67 mpoeq3ia 
 |-  ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) ) )
69 68 mpteq2i 
 |-  ( 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 ) ) ) ) ) ) = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) ) ) )
70 1 69 eqtri 
 |-  L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( a ` l ) [,) ( b ` l ) ) ) ) ) )
71 70 33 38 41 hoidmvcl 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` X ) ( D ` j ) ) e. ( 0 [,) +oo ) )
72 eqid 
 |-  ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) )
73 71 72 fmptd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) : NN --> ( 0 [,) +oo ) )
74 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
75 74 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
76 73 75 fssd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) : NN --> ( 0 [,] +oo ) )
77 59 76 feq1dd 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) : NN --> ( 0 [,] +oo ) )
78 77 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) : NN --> ( 0 [,] +oo ) )
79 28 78 sge0repnf 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) )
80 26 79 mpbird 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR )
81 13 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( A ` Z ) e. RR )
82 12 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( B ` Z ) e. RR )
83 simplr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( A ` Z ) < ( B ` Z ) )
84 eqid 
 |-  ( j e. NN |-> ( ( C ` j ) ` Z ) ) = ( j e. NN |-> ( ( C ` j ) ` Z ) )
85 47 84 fmptd 
 |-  ( ph -> ( j e. NN |-> ( ( C ` j ) ` Z ) ) : NN --> RR )
86 85 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( j e. NN |-> ( ( C ` j ) ` Z ) ) : NN --> RR )
87 eqid 
 |-  ( j e. NN |-> ( ( D ` j ) ` Z ) ) = ( j e. NN |-> ( ( D ` j ) ` Z ) )
88 48 87 fmptd 
 |-  ( ph -> ( j e. NN |-> ( ( D ` j ) ` Z ) ) : NN --> RR )
89 88 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( j e. NN |-> ( ( D ` j ) ` Z ) ) : NN --> RR )
90 3 eleq2i 
 |-  ( k e. X <-> k e. { Z } )
91 90 biimpi 
 |-  ( k e. X -> k e. { Z } )
92 elsni 
 |-  ( k e. { Z } -> k = Z )
93 91 92 syl 
 |-  ( k e. X -> k = Z )
94 93 54 syl 
 |-  ( k e. X -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
95 94 rgen 
 |-  A. k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) )
96 ixpeq2 
 |-  ( A. k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
97 95 96 ax-mp 
 |-  X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) )
98 97 a1i 
 |-  ( j e. NN -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
99 98 iuneq2i 
 |-  U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) )
100 99 a1i 
 |-  ( ph -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
101 8 100 sseqtrd 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
102 101 adantr 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
103 id 
 |-  ( x e. ( ( A ` Z ) [,) ( B ` Z ) ) -> x e. ( ( A ` Z ) [,) ( B ` Z ) ) )
104 eqidd 
 |-  ( x e. ( ( A ` Z ) [,) ( B ` Z ) ) -> { <. Z , x >. } = { <. Z , x >. } )
105 opeq2 
 |-  ( y = x -> <. Z , y >. = <. Z , x >. )
106 105 sneqd 
 |-  ( y = x -> { <. Z , y >. } = { <. Z , x >. } )
107 106 rspceeqv 
 |-  ( ( x e. ( ( A ` Z ) [,) ( B ` Z ) ) /\ { <. Z , x >. } = { <. Z , x >. } ) -> E. y e. ( ( A ` Z ) [,) ( B ` Z ) ) { <. Z , x >. } = { <. Z , y >. } )
108 103 104 107 syl2anc 
 |-  ( x e. ( ( A ` Z ) [,) ( B ` Z ) ) -> E. y e. ( ( A ` Z ) [,) ( B ` Z ) ) { <. Z , x >. } = { <. Z , y >. } )
109 108 adantl 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> E. y e. ( ( A ` Z ) [,) ( B ` Z ) ) { <. Z , x >. } = { <. Z , y >. } )
110 elixpsn 
 |-  ( Z e. V -> ( { <. Z , x >. } e. X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) <-> E. y e. ( ( A ` Z ) [,) ( B ` Z ) ) { <. Z , x >. } = { <. Z , y >. } ) )
111 2 110 syl 
 |-  ( ph -> ( { <. Z , x >. } e. X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) <-> E. y e. ( ( A ` Z ) [,) ( B ` Z ) ) { <. Z , x >. } = { <. Z , y >. } ) )
112 111 adantr 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> ( { <. Z , x >. } e. X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) <-> E. y e. ( ( A ` Z ) [,) ( B ` Z ) ) { <. Z , x >. } = { <. Z , y >. } ) )
113 109 112 mpbird 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> { <. Z , x >. } e. X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) )
114 3 eqcomi 
 |-  { Z } = X
115 ixpeq1 
 |-  ( { Z } = X -> X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` Z ) [,) ( B ` Z ) ) )
116 114 115 ax-mp 
 |-  X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` Z ) [,) ( B ` Z ) )
117 fveq2 
 |-  ( k = Z -> ( A ` k ) = ( A ` Z ) )
118 93 117 syl 
 |-  ( k e. X -> ( A ` k ) = ( A ` Z ) )
119 fveq2 
 |-  ( k = Z -> ( B ` k ) = ( B ` Z ) )
120 93 119 syl 
 |-  ( k e. X -> ( B ` k ) = ( B ` Z ) )
121 118 120 oveq12d 
 |-  ( k e. X -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
122 121 eqcomd 
 |-  ( k e. X -> ( ( A ` Z ) [,) ( B ` Z ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
123 122 rgen 
 |-  A. k e. X ( ( A ` Z ) [,) ( B ` Z ) ) = ( ( A ` k ) [,) ( B ` k ) )
124 ixpeq2 
 |-  ( A. k e. X ( ( A ` Z ) [,) ( B ` Z ) ) = ( ( A ` k ) [,) ( B ` k ) ) -> X_ k e. X ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
125 123 124 ax-mp 
 |-  X_ k e. X ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
126 116 125 eqtri 
 |-  X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
127 126 a1i 
 |-  ( ph -> X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
128 127 adantr 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> X_ k e. { Z } ( ( A ` Z ) [,) ( B ` Z ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
129 113 128 eleqtrd 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> { <. Z , x >. } e. X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
130 102 129 sseldd 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> { <. Z , x >. } e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
131 eliun 
 |-  ( { <. Z , x >. } e. U_ j e. NN X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> E. j e. NN { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
132 130 131 sylib 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> E. j e. NN { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
133 ixpeq1 
 |-  ( X = { Z } -> X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
134 3 133 ax-mp 
 |-  X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) )
135 134 eleq2i 
 |-  ( { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> { <. Z , x >. } e. X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
136 135 biimpi 
 |-  ( { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> { <. Z , x >. } e. X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
137 136 adantl 
 |-  ( ( ph /\ { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> { <. Z , x >. } e. X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
138 elixpsn 
 |-  ( Z e. V -> ( { <. Z , x >. } e. X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> E. y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) { <. Z , x >. } = { <. Z , y >. } ) )
139 2 138 syl 
 |-  ( ph -> ( { <. Z , x >. } e. X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> E. y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) { <. Z , x >. } = { <. Z , y >. } ) )
140 139 adantr 
 |-  ( ( ph /\ { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( { <. Z , x >. } e. X_ k e. { Z } ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> E. y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) { <. Z , x >. } = { <. Z , y >. } ) )
141 137 140 mpbid 
 |-  ( ( ph /\ { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> E. y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) { <. Z , x >. } = { <. Z , y >. } )
142 opex 
 |-  <. Z , x >. e. _V
143 142 sneqr 
 |-  ( { <. Z , x >. } = { <. Z , y >. } -> <. Z , x >. = <. Z , y >. )
144 143 adantl 
 |-  ( ( ph /\ { <. Z , x >. } = { <. Z , y >. } ) -> <. Z , x >. = <. Z , y >. )
145 vex 
 |-  x e. _V
146 145 a1i 
 |-  ( ph -> x e. _V )
147 opthg 
 |-  ( ( Z e. V /\ x e. _V ) -> ( <. Z , x >. = <. Z , y >. <-> ( Z = Z /\ x = y ) ) )
148 2 146 147 syl2anc 
 |-  ( ph -> ( <. Z , x >. = <. Z , y >. <-> ( Z = Z /\ x = y ) ) )
149 148 adantr 
 |-  ( ( ph /\ { <. Z , x >. } = { <. Z , y >. } ) -> ( <. Z , x >. = <. Z , y >. <-> ( Z = Z /\ x = y ) ) )
150 144 149 mpbid 
 |-  ( ( ph /\ { <. Z , x >. } = { <. Z , y >. } ) -> ( Z = Z /\ x = y ) )
151 150 simprd 
 |-  ( ( ph /\ { <. Z , x >. } = { <. Z , y >. } ) -> x = y )
152 151 3adant2 
 |-  ( ( ph /\ y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) /\ { <. Z , x >. } = { <. Z , y >. } ) -> x = y )
153 simp2 
 |-  ( ( ph /\ y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) /\ { <. Z , x >. } = { <. Z , y >. } ) -> y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
154 152 153 eqeltrd 
 |-  ( ( ph /\ y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) /\ { <. Z , x >. } = { <. Z , y >. } ) -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
155 154 3exp 
 |-  ( ph -> ( y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> ( { <. Z , x >. } = { <. Z , y >. } -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) )
156 155 adantr 
 |-  ( ( ph /\ { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> ( { <. Z , x >. } = { <. Z , y >. } -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) )
157 156 rexlimdv 
 |-  ( ( ph /\ { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( E. y e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) { <. Z , x >. } = { <. Z , y >. } -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
158 141 157 mpd 
 |-  ( ( ph /\ { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
159 158 ex 
 |-  ( ph -> ( { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
160 159 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) /\ j e. NN ) -> ( { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
161 160 reximdva 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> ( E. j e. NN { <. Z , x >. } e. X_ k e. X ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> E. j e. NN x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
162 132 161 mpd 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> E. j e. NN x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
163 eliun 
 |-  ( x e. U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> E. j e. NN x e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
164 162 163 sylibr 
 |-  ( ( ph /\ x e. ( ( A ` Z ) [,) ( B ` Z ) ) ) -> x e. U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
165 164 ralrimiva 
 |-  ( ph -> A. x e. ( ( A ` Z ) [,) ( B ` Z ) ) x e. U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
166 dfss3 
 |-  ( ( ( A ` Z ) [,) ( B ` Z ) ) C_ U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> A. x e. ( ( A ` Z ) [,) ( B ` Z ) ) x e. U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
167 165 166 sylibr 
 |-  ( ph -> ( ( A ` Z ) [,) ( B ` Z ) ) C_ U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
168 eqidd 
 |-  ( ( ph /\ i e. NN ) -> ( j e. NN |-> ( ( C ` j ) ` Z ) ) = ( j e. NN |-> ( ( C ` j ) ` Z ) ) )
169 fveq2 
 |-  ( j = i -> ( C ` j ) = ( C ` i ) )
170 169 fveq1d 
 |-  ( j = i -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
171 170 adantl 
 |-  ( ( ( ph /\ i e. NN ) /\ j = i ) -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
172 simpr 
 |-  ( ( ph /\ i e. NN ) -> i e. NN )
173 fvexd 
 |-  ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. _V )
174 168 171 172 173 fvmptd 
 |-  ( ( ph /\ i e. NN ) -> ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) = ( ( C ` i ) ` Z ) )
175 eqidd 
 |-  ( ( ph /\ i e. NN ) -> ( j e. NN |-> ( ( D ` j ) ` Z ) ) = ( j e. NN |-> ( ( D ` j ) ` Z ) ) )
176 fveq2 
 |-  ( j = i -> ( D ` j ) = ( D ` i ) )
177 176 fveq1d 
 |-  ( j = i -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
178 177 adantl 
 |-  ( ( ( ph /\ i e. NN ) /\ j = i ) -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
179 fvexd 
 |-  ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. _V )
180 175 178 172 179 fvmptd 
 |-  ( ( ph /\ i e. NN ) -> ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) = ( ( D ` i ) ` Z ) )
181 174 180 oveq12d 
 |-  ( ( ph /\ i e. NN ) -> ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
182 181 iuneq2dv 
 |-  ( ph -> U_ i e. NN ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) = U_ i e. NN ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
183 170 177 oveq12d 
 |-  ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
184 183 cbviunv 
 |-  U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = U_ i e. NN ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) )
185 184 eqcomi 
 |-  U_ i e. NN ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) )
186 185 a1i 
 |-  ( ph -> U_ i e. NN ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
187 182 186 eqtr2d 
 |-  ( ph -> U_ j e. NN ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = U_ i e. NN ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) )
188 167 187 sseqtrd 
 |-  ( ph -> ( ( A ` Z ) [,) ( B ` Z ) ) C_ U_ i e. NN ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) )
189 188 ad2antrr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( ( A ` Z ) [,) ( B ` Z ) ) C_ U_ i e. NN ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) )
190 fvex 
 |-  ( ( C ` i ) ` Z ) e. _V
191 170 84 190 fvmpt 
 |-  ( i e. NN -> ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) = ( ( C ` i ) ` Z ) )
192 fvex 
 |-  ( ( D ` i ) ` Z ) e. _V
193 177 87 192 fvmpt 
 |-  ( i e. NN -> ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) = ( ( D ` i ) ` Z ) )
194 191 193 oveq12d 
 |-  ( i e. NN -> ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
195 194 fveq2d 
 |-  ( i e. NN -> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) = ( vol ` ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
196 195 mpteq2ia 
 |-  ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) ) = ( i e. NN |-> ( vol ` ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
197 eqcom 
 |-  ( j = i <-> i = j )
198 197 imbi1i 
 |-  ( ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) <-> ( i = j -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
199 eqcom 
 |-  ( ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) <-> ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
200 199 imbi2i 
 |-  ( ( i = j -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) <-> ( i = j -> ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
201 198 200 bitri 
 |-  ( ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) <-> ( i = j -> ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
202 183 201 mpbi 
 |-  ( i = j -> ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
203 202 fveq2d 
 |-  ( i = j -> ( vol ` ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) = ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
204 203 cbvmptv 
 |-  ( i e. NN |-> ( vol ` ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
205 196 204 eqtri 
 |-  ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) ) = ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
206 205 fveq2i 
 |-  ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) )
207 206 a1i 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
208 simpr 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR )
209 207 208 eqeltrd 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) ) ) e. RR )
210 oveq1 
 |-  ( w = z -> ( w - ( A ` Z ) ) = ( z - ( A ` Z ) ) )
211 193 breq1d 
 |-  ( i e. NN -> ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z <-> ( ( D ` i ) ` Z ) <_ z ) )
212 211 193 ifbieq1d 
 |-  ( i e. NN -> if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) = if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) )
213 191 212 oveq12d 
 |-  ( i e. NN -> ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) = ( ( ( C ` i ) ` Z ) [,) if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) ) )
214 213 fveq2d 
 |-  ( i e. NN -> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) = ( vol ` ( ( ( C ` i ) ` Z ) [,) if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) ) ) )
215 214 mpteq2ia 
 |-  ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) = ( i e. NN |-> ( vol ` ( ( ( C ` i ) ` Z ) [,) if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) ) ) )
216 fveq2 
 |-  ( i = h -> ( C ` i ) = ( C ` h ) )
217 216 fveq1d 
 |-  ( i = h -> ( ( C ` i ) ` Z ) = ( ( C ` h ) ` Z ) )
218 fveq2 
 |-  ( i = h -> ( D ` i ) = ( D ` h ) )
219 218 fveq1d 
 |-  ( i = h -> ( ( D ` i ) ` Z ) = ( ( D ` h ) ` Z ) )
220 219 breq1d 
 |-  ( i = h -> ( ( ( D ` i ) ` Z ) <_ z <-> ( ( D ` h ) ` Z ) <_ z ) )
221 220 219 ifbieq1d 
 |-  ( i = h -> if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) = if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) )
222 217 221 oveq12d 
 |-  ( i = h -> ( ( ( C ` i ) ` Z ) [,) if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) ) = ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) )
223 222 fveq2d 
 |-  ( i = h -> ( vol ` ( ( ( C ` i ) ` Z ) [,) if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) ) ) = ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) ) )
224 223 cbvmptv 
 |-  ( i e. NN |-> ( vol ` ( ( ( C ` i ) ` Z ) [,) if ( ( ( D ` i ) ` Z ) <_ z , ( ( D ` i ) ` Z ) , z ) ) ) ) = ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) ) )
225 215 224 eqtri 
 |-  ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) = ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) ) )
226 225 a1i 
 |-  ( w = z -> ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) = ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) ) ) )
227 breq2 
 |-  ( w = z -> ( ( ( D ` h ) ` Z ) <_ w <-> ( ( D ` h ) ` Z ) <_ z ) )
228 id 
 |-  ( w = z -> w = z )
229 227 228 ifbieq2d 
 |-  ( w = z -> if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) = if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) )
230 229 eqcomd 
 |-  ( w = z -> if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) = if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) )
231 230 oveq2d 
 |-  ( w = z -> ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) = ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) )
232 231 fveq2d 
 |-  ( w = z -> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) ) = ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) )
233 232 mpteq2dv 
 |-  ( w = z -> ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ z , ( ( D ` h ) ` Z ) , z ) ) ) ) = ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) )
234 226 233 eqtr2d 
 |-  ( w = z -> ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) = ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) )
235 234 fveq2d 
 |-  ( w = z -> ( sum^ ` ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) ) = ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) ) )
236 210 235 breq12d 
 |-  ( w = z -> ( ( w - ( A ` Z ) ) <_ ( sum^ ` ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) ) <-> ( z - ( A ` Z ) ) <_ ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) ) ) )
237 236 cbvrabv 
 |-  { w e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( w - ( A ` Z ) ) <_ ( sum^ ` ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) ) } = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( z - ( A ` Z ) ) <_ ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) if ( ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) <_ z , ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) , z ) ) ) ) ) }
238 eqid 
 |-  sup ( { w e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( w - ( A ` Z ) ) <_ ( sum^ ` ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) ) } , RR , < ) = sup ( { w e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( w - ( A ` Z ) ) <_ ( sum^ ` ( h e. NN |-> ( vol ` ( ( ( C ` h ) ` Z ) [,) if ( ( ( D ` h ) ` Z ) <_ w , ( ( D ` h ) ` Z ) , w ) ) ) ) ) } , RR , < )
239 81 82 83 86 89 189 209 237 238 hoidmv1lelem3 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( ( B ` Z ) - ( A ` Z ) ) <_ ( sum^ ` ( i e. NN |-> ( vol ` ( ( ( j e. NN |-> ( ( C ` j ) ` Z ) ) ` i ) [,) ( ( j e. NN |-> ( ( D ` j ) ` Z ) ) ` i ) ) ) ) ) )
240 239 207 breqtrd 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) e. RR ) -> ( ( B ` Z ) - ( A ` Z ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
241 25 80 240 syl2anc 
 |-  ( ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) /\ -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) = +oo ) -> ( ( B ` Z ) - ( A ` Z ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
242 24 241 pm2.61dan 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( ( B ` Z ) - ( A ` Z ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
243 1 32 34 4 5 hoidmvn0val 
 |-  ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
244 29 prodeq1d 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. { Z } ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
245 volicore 
 |-  ( ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR ) -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. RR )
246 13 12 245 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. RR )
247 246 recnd 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. CC )
248 117 119 oveq12d 
 |-  ( k = Z -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
249 248 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
250 249 prodsn 
 |-  ( ( Z e. V /\ ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. CC ) -> prod_ k e. { Z } ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
251 2 247 250 syl2anc 
 |-  ( ph -> prod_ k e. { Z } ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
252 243 244 251 3eqtrd 
 |-  ( ph -> ( A ( L ` X ) B ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
253 252 adantr 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( A ( L ` X ) B ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
254 volico 
 |-  ( ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR ) -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) = if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) )
255 13 12 254 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) = if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) )
256 255 adantr 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) = if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) )
257 iftrue 
 |-  ( ( A ` Z ) < ( B ` Z ) -> if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) = ( ( B ` Z ) - ( A ` Z ) ) )
258 257 adantl 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) = ( ( B ` Z ) - ( A ` Z ) ) )
259 253 256 258 3eqtrd 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( A ( L ` X ) B ) = ( ( B ` Z ) - ( A ` Z ) ) )
260 59 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
261 260 adantr 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) )
262 259 261 breq12d 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) <-> ( ( B ` Z ) - ( A ` Z ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) ) ) ) )
263 242 262 mpbird 
 |-  ( ( ph /\ ( A ` Z ) < ( B ` Z ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
264 243 adantr 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
265 244 adantr 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. { Z } ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
266 251 adantr 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> prod_ k e. { Z } ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
267 255 adantr 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) = if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) )
268 iffalse 
 |-  ( -. ( A ` Z ) < ( B ` Z ) -> if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) = 0 )
269 268 adantl 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> if ( ( A ` Z ) < ( B ` Z ) , ( ( B ` Z ) - ( A ` Z ) ) , 0 ) = 0 )
270 266 267 269 3eqtrd 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> prod_ k e. { Z } ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
271 264 265 270 3eqtrd 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> ( A ( L ` X ) B ) = 0 )
272 27 a1i 
 |-  ( ph -> NN e. _V )
273 272 76 sge0ge0 
 |-  ( ph -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
274 273 adantr 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
275 271 274 eqbrtrd 
 |-  ( ( ph /\ -. ( A ` Z ) < ( B ` Z ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
276 263 275 pm2.61dan 
 |-  ( ph -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )