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
|
ffvelrnd |
|- ( ph -> ( B ` Z ) e. RR ) |
13 |
4 11
|
ffvelrnd |
|- ( 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
|
ffvelrnda |
|- ( ( 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
|
ffvelrnda |
|- ( ( 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
|
ffvelrnd |
|- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR ) |
48 |
41 46
|
ffvelrnd |
|- ( ( 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 ) ) ) ) ) |