Step |
Hyp |
Ref |
Expression |
1 |
|
uniioombl.1 |
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
2 |
|
uniioombl.2 |
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) |
3 |
|
uniioombl.3 |
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) ) |
4 |
|
uniioombl.a |
|- A = U. ran ( (,) o. F ) |
5 |
|
uniioombl.e |
|- ( ph -> ( vol* ` E ) e. RR ) |
6 |
|
uniioombl.c |
|- ( ph -> C e. RR+ ) |
7 |
|
uniioombl.g |
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
8 |
|
uniioombl.s |
|- ( ph -> E C_ U. ran ( (,) o. G ) ) |
9 |
|
uniioombl.t |
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) ) |
10 |
|
uniioombl.v |
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) ) |
11 |
|
uniioombllem2.h |
|- H = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
12 |
|
uniioombllem2.k |
|- K = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) ) |
13 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
14 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) |
15 |
|
1zzd |
|- ( ( ph /\ J e. NN ) -> 1 e. ZZ ) |
16 |
|
eqidd |
|- ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) = ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) ) |
17 |
1 2 3 4 5 6 7 8 9 10
|
uniioombllem2a |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) ) |
18 |
11
|
a1i |
|- ( ( ph /\ J e. NN ) -> H = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
19 |
12
|
ioorf |
|- K : ran (,) --> ( <_ i^i ( RR* X. RR* ) ) |
20 |
19
|
a1i |
|- ( ( ph /\ J e. NN ) -> K : ran (,) --> ( <_ i^i ( RR* X. RR* ) ) ) |
21 |
20
|
feqmptd |
|- ( ( ph /\ J e. NN ) -> K = ( y e. ran (,) |-> ( K ` y ) ) ) |
22 |
|
fveq2 |
|- ( y = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) -> ( K ` y ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
23 |
17 18 21 22
|
fmptco |
|- ( ( ph /\ J e. NN ) -> ( K o. H ) = ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) |
24 |
|
inss2 |
|- ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) C_ ( (,) ` ( G ` J ) ) |
25 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
26 |
7
|
ffvelrnda |
|- ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( <_ i^i ( RR X. RR ) ) ) |
27 |
25 26
|
sselid |
|- ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( RR X. RR ) ) |
28 |
|
1st2nd2 |
|- ( ( G ` J ) e. ( RR X. RR ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) |
29 |
27 28
|
syl |
|- ( ( ph /\ J e. NN ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) |
30 |
29
|
fveq2d |
|- ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) ) |
31 |
|
df-ov |
|- ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) |
32 |
30 31
|
eqtr4di |
|- ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) |
33 |
|
ioossre |
|- ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) C_ RR |
34 |
32 33
|
eqsstrdi |
|- ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) C_ RR ) |
35 |
32
|
fveq2d |
|- ( ( ph /\ J e. NN ) -> ( vol* ` ( (,) ` ( G ` J ) ) ) = ( vol* ` ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) ) |
36 |
|
ovolfcl |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) ) |
37 |
7 36
|
sylan |
|- ( ( ph /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) ) |
38 |
|
ovolioo |
|- ( ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) -> ( vol* ` ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) ) |
39 |
37 38
|
syl |
|- ( ( ph /\ J e. NN ) -> ( vol* ` ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) ) |
40 |
35 39
|
eqtrd |
|- ( ( ph /\ J e. NN ) -> ( vol* ` ( (,) ` ( G ` J ) ) ) = ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) ) |
41 |
37
|
simp2d |
|- ( ( ph /\ J e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR ) |
42 |
37
|
simp1d |
|- ( ( ph /\ J e. NN ) -> ( 1st ` ( G ` J ) ) e. RR ) |
43 |
41 42
|
resubcld |
|- ( ( ph /\ J e. NN ) -> ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) e. RR ) |
44 |
40 43
|
eqeltrd |
|- ( ( ph /\ J e. NN ) -> ( vol* ` ( (,) ` ( G ` J ) ) ) e. RR ) |
45 |
|
ovolsscl |
|- ( ( ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) C_ ( (,) ` ( G ` J ) ) /\ ( (,) ` ( G ` J ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` J ) ) ) e. RR ) -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR ) |
46 |
24 34 44 45
|
mp3an2i |
|- ( ( ph /\ J e. NN ) -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR ) |
47 |
46
|
adantr |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR ) |
48 |
12
|
ioorcl |
|- ( ( ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) /\ ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR ) -> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. ( <_ i^i ( RR X. RR ) ) ) |
49 |
17 47 48
|
syl2anc |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. ( <_ i^i ( RR X. RR ) ) ) |
50 |
23 49
|
fmpt3d |
|- ( ( ph /\ J e. NN ) -> ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) ) |
51 |
|
eqid |
|- ( ( abs o. - ) o. ( K o. H ) ) = ( ( abs o. - ) o. ( K o. H ) ) |
52 |
51
|
ovolfsf |
|- ( ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. ( K o. H ) ) : NN --> ( 0 [,) +oo ) ) |
53 |
50 52
|
syl |
|- ( ( ph /\ J e. NN ) -> ( ( abs o. - ) o. ( K o. H ) ) : NN --> ( 0 [,) +oo ) ) |
54 |
53
|
ffvelrnda |
|- ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. ( 0 [,) +oo ) ) |
55 |
|
elrege0 |
|- ( ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) ) ) |
56 |
54 55
|
sylib |
|- ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) ) ) |
57 |
56
|
simpld |
|- ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. RR ) |
58 |
56
|
simprd |
|- ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) ) |
59 |
23
|
fveq1d |
|- ( ( ph /\ J e. NN ) -> ( ( K o. H ) ` z ) = ( ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ` z ) ) |
60 |
|
fvex |
|- ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. _V |
61 |
|
eqid |
|- ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) = ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
62 |
61
|
fvmpt2 |
|- ( ( z e. NN /\ ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. _V ) -> ( ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ` z ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
63 |
60 62
|
mpan2 |
|- ( z e. NN -> ( ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ` z ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
64 |
59 63
|
sylan9eq |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( K o. H ) ` z ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
65 |
64
|
fveq2d |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( ( K o. H ) ` z ) ) = ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) |
66 |
12
|
ioorinv |
|- ( ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) -> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
67 |
17 66
|
syl |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
68 |
65 67
|
eqtrd |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
69 |
68
|
ralrimiva |
|- ( ( ph /\ J e. NN ) -> A. z e. NN ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
70 |
|
2fveq3 |
|- ( z = x -> ( (,) ` ( ( K o. H ) ` z ) ) = ( (,) ` ( ( K o. H ) ` x ) ) ) |
71 |
|
2fveq3 |
|- ( z = x -> ( (,) ` ( F ` z ) ) = ( (,) ` ( F ` x ) ) ) |
72 |
71
|
ineq1d |
|- ( z = x -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
73 |
70 72
|
eqeq12d |
|- ( z = x -> ( ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) <-> ( (,) ` ( ( K o. H ) ` x ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
74 |
73
|
rspccva |
|- ( ( A. z e. NN ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) /\ x e. NN ) -> ( (,) ` ( ( K o. H ) ` x ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
75 |
69 74
|
sylan |
|- ( ( ( ph /\ J e. NN ) /\ x e. NN ) -> ( (,) ` ( ( K o. H ) ` x ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
76 |
|
inss1 |
|- ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) C_ ( (,) ` ( F ` x ) ) |
77 |
75 76
|
eqsstrdi |
|- ( ( ( ph /\ J e. NN ) /\ x e. NN ) -> ( (,) ` ( ( K o. H ) ` x ) ) C_ ( (,) ` ( F ` x ) ) ) |
78 |
77
|
ralrimiva |
|- ( ( ph /\ J e. NN ) -> A. x e. NN ( (,) ` ( ( K o. H ) ` x ) ) C_ ( (,) ` ( F ` x ) ) ) |
79 |
2
|
adantr |
|- ( ( ph /\ J e. NN ) -> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) |
80 |
|
disjss2 |
|- ( A. x e. NN ( (,) ` ( ( K o. H ) ` x ) ) C_ ( (,) ` ( F ` x ) ) -> ( Disj_ x e. NN ( (,) ` ( F ` x ) ) -> Disj_ x e. NN ( (,) ` ( ( K o. H ) ` x ) ) ) ) |
81 |
78 79 80
|
sylc |
|- ( ( ph /\ J e. NN ) -> Disj_ x e. NN ( (,) ` ( ( K o. H ) ` x ) ) ) |
82 |
50 81 14
|
uniioovol |
|- ( ( ph /\ J e. NN ) -> ( vol* ` U. ran ( (,) o. ( K o. H ) ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) ) |
83 |
67
|
mpteq2dva |
|- ( ( ph /\ J e. NN ) -> ( z e. NN |-> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) |
84 |
|
rexpssxrxp |
|- ( RR X. RR ) C_ ( RR* X. RR* ) |
85 |
25 84
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) |
86 |
85 49
|
sselid |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. ( RR* X. RR* ) ) |
87 |
|
ioof |
|- (,) : ( RR* X. RR* ) --> ~P RR |
88 |
87
|
a1i |
|- ( ( ph /\ J e. NN ) -> (,) : ( RR* X. RR* ) --> ~P RR ) |
89 |
88
|
feqmptd |
|- ( ( ph /\ J e. NN ) -> (,) = ( y e. ( RR* X. RR* ) |-> ( (,) ` y ) ) ) |
90 |
|
fveq2 |
|- ( y = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) -> ( (,) ` y ) = ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) |
91 |
86 23 89 90
|
fmptco |
|- ( ( ph /\ J e. NN ) -> ( (,) o. ( K o. H ) ) = ( z e. NN |-> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) ) |
92 |
83 91 18
|
3eqtr4d |
|- ( ( ph /\ J e. NN ) -> ( (,) o. ( K o. H ) ) = H ) |
93 |
92
|
rneqd |
|- ( ( ph /\ J e. NN ) -> ran ( (,) o. ( K o. H ) ) = ran H ) |
94 |
93
|
unieqd |
|- ( ( ph /\ J e. NN ) -> U. ran ( (,) o. ( K o. H ) ) = U. ran H ) |
95 |
|
fvex |
|- ( (,) ` ( F ` z ) ) e. _V |
96 |
95
|
inex1 |
|- ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. _V |
97 |
11
|
fvmpt2 |
|- ( ( z e. NN /\ ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. _V ) -> ( H ` z ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
98 |
96 97
|
mpan2 |
|- ( z e. NN -> ( H ` z ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) |
99 |
|
incom |
|- ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) ) |
100 |
98 99
|
eqtrdi |
|- ( z e. NN -> ( H ` z ) = ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) ) ) |
101 |
100
|
iuneq2i |
|- U_ z e. NN ( H ` z ) = U_ z e. NN ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) ) |
102 |
|
iunin2 |
|- U_ z e. NN ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) ) = ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) ) |
103 |
101 102
|
eqtri |
|- U_ z e. NN ( H ` z ) = ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) ) |
104 |
17 11
|
fmptd |
|- ( ( ph /\ J e. NN ) -> H : NN --> ran (,) ) |
105 |
104
|
ffnd |
|- ( ( ph /\ J e. NN ) -> H Fn NN ) |
106 |
|
fniunfv |
|- ( H Fn NN -> U_ z e. NN ( H ` z ) = U. ran H ) |
107 |
105 106
|
syl |
|- ( ( ph /\ J e. NN ) -> U_ z e. NN ( H ` z ) = U. ran H ) |
108 |
103 107
|
eqtr3id |
|- ( ( ph /\ J e. NN ) -> ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) ) = U. ran H ) |
109 |
1
|
adantr |
|- ( ( ph /\ J e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
110 |
|
fvco3 |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ z e. NN ) -> ( ( (,) o. F ) ` z ) = ( (,) ` ( F ` z ) ) ) |
111 |
109 110
|
sylan |
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) o. F ) ` z ) = ( (,) ` ( F ` z ) ) ) |
112 |
111
|
iuneq2dv |
|- ( ( ph /\ J e. NN ) -> U_ z e. NN ( ( (,) o. F ) ` z ) = U_ z e. NN ( (,) ` ( F ` z ) ) ) |
113 |
|
ffn |
|- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) ) |
114 |
87 113
|
ax-mp |
|- (,) Fn ( RR* X. RR* ) |
115 |
|
fss |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) ) |
116 |
109 85 115
|
sylancl |
|- ( ( ph /\ J e. NN ) -> F : NN --> ( RR* X. RR* ) ) |
117 |
|
fnfco |
|- ( ( (,) Fn ( RR* X. RR* ) /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) Fn NN ) |
118 |
114 116 117
|
sylancr |
|- ( ( ph /\ J e. NN ) -> ( (,) o. F ) Fn NN ) |
119 |
|
fniunfv |
|- ( ( (,) o. F ) Fn NN -> U_ z e. NN ( ( (,) o. F ) ` z ) = U. ran ( (,) o. F ) ) |
120 |
118 119
|
syl |
|- ( ( ph /\ J e. NN ) -> U_ z e. NN ( ( (,) o. F ) ` z ) = U. ran ( (,) o. F ) ) |
121 |
120 4
|
eqtr4di |
|- ( ( ph /\ J e. NN ) -> U_ z e. NN ( ( (,) o. F ) ` z ) = A ) |
122 |
112 121
|
eqtr3d |
|- ( ( ph /\ J e. NN ) -> U_ z e. NN ( (,) ` ( F ` z ) ) = A ) |
123 |
122
|
ineq2d |
|- ( ( ph /\ J e. NN ) -> ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) ) = ( ( (,) ` ( G ` J ) ) i^i A ) ) |
124 |
94 108 123
|
3eqtr2d |
|- ( ( ph /\ J e. NN ) -> U. ran ( (,) o. ( K o. H ) ) = ( ( (,) ` ( G ` J ) ) i^i A ) ) |
125 |
124
|
fveq2d |
|- ( ( ph /\ J e. NN ) -> ( vol* ` U. ran ( (,) o. ( K o. H ) ) ) = ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) ) |
126 |
82 125
|
eqtr3d |
|- ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) = ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) ) |
127 |
|
inss1 |
|- ( ( (,) ` ( G ` J ) ) i^i A ) C_ ( (,) ` ( G ` J ) ) |
128 |
|
ovolsscl |
|- ( ( ( ( (,) ` ( G ` J ) ) i^i A ) C_ ( (,) ` ( G ` J ) ) /\ ( (,) ` ( G ` J ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` J ) ) ) e. RR ) -> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) e. RR ) |
129 |
127 34 44 128
|
mp3an2i |
|- ( ( ph /\ J e. NN ) -> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) e. RR ) |
130 |
126 129
|
eqeltrd |
|- ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) e. RR ) |
131 |
51 14
|
ovolsf |
|- ( ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) : NN --> ( 0 [,) +oo ) ) |
132 |
50 131
|
syl |
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) : NN --> ( 0 [,) +oo ) ) |
133 |
132
|
frnd |
|- ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ ( 0 [,) +oo ) ) |
134 |
|
icossxr |
|- ( 0 [,) +oo ) C_ RR* |
135 |
133 134
|
sstrdi |
|- ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR* ) |
136 |
132
|
ffnd |
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) Fn NN ) |
137 |
|
fnfvelrn |
|- ( ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) Fn NN /\ y e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ) |
138 |
136 137
|
sylan |
|- ( ( ( ph /\ J e. NN ) /\ y e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ) |
139 |
|
supxrub |
|- ( ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR* /\ ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) ) |
140 |
135 138 139
|
syl2an2r |
|- ( ( ( ph /\ J e. NN ) /\ y e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) ) |
141 |
140
|
ralrimiva |
|- ( ( ph /\ J e. NN ) -> A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) ) |
142 |
|
brralrspcev |
|- ( ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) e. RR /\ A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) ) -> E. x e. RR A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) |
143 |
130 141 142
|
syl2anc |
|- ( ( ph /\ J e. NN ) -> E. x e. RR A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) |
144 |
13 14 15 16 57 58 143
|
isumsup2 |
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ~~> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) ) |
145 |
51
|
ovolfs2 |
|- ( ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. ( K o. H ) ) = ( ( vol* o. (,) ) o. ( K o. H ) ) ) |
146 |
50 145
|
syl |
|- ( ( ph /\ J e. NN ) -> ( ( abs o. - ) o. ( K o. H ) ) = ( ( vol* o. (,) ) o. ( K o. H ) ) ) |
147 |
|
coass |
|- ( ( vol* o. (,) ) o. ( K o. H ) ) = ( vol* o. ( (,) o. ( K o. H ) ) ) |
148 |
92
|
coeq2d |
|- ( ( ph /\ J e. NN ) -> ( vol* o. ( (,) o. ( K o. H ) ) ) = ( vol* o. H ) ) |
149 |
147 148
|
eqtrid |
|- ( ( ph /\ J e. NN ) -> ( ( vol* o. (,) ) o. ( K o. H ) ) = ( vol* o. H ) ) |
150 |
146 149
|
eqtrd |
|- ( ( ph /\ J e. NN ) -> ( ( abs o. - ) o. ( K o. H ) ) = ( vol* o. H ) ) |
151 |
150
|
seqeq3d |
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = seq 1 ( + , ( vol* o. H ) ) ) |
152 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
153 |
133 152
|
sstrdi |
|- ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR ) |
154 |
|
1nn |
|- 1 e. NN |
155 |
132
|
fdmd |
|- ( ( ph /\ J e. NN ) -> dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = NN ) |
156 |
154 155
|
eleqtrrid |
|- ( ( ph /\ J e. NN ) -> 1 e. dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ) |
157 |
156
|
ne0d |
|- ( ( ph /\ J e. NN ) -> dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) ) |
158 |
|
dm0rn0 |
|- ( dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = (/) <-> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = (/) ) |
159 |
158
|
necon3bii |
|- ( dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) <-> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) ) |
160 |
157 159
|
sylib |
|- ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) ) |
161 |
|
breq1 |
|- ( z = ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) -> ( z <_ x <-> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) ) |
162 |
161
|
ralrn |
|- ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) Fn NN -> ( A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x <-> A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) ) |
163 |
136 162
|
syl |
|- ( ( ph /\ J e. NN ) -> ( A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x <-> A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) ) |
164 |
163
|
rexbidv |
|- ( ( ph /\ J e. NN ) -> ( E. x e. RR A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x <-> E. x e. RR A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) ) |
165 |
143 164
|
mpbird |
|- ( ( ph /\ J e. NN ) -> E. x e. RR A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x ) |
166 |
|
supxrre |
|- ( ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR /\ ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) /\ E. x e. RR A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) ) |
167 |
153 160 165 166
|
syl3anc |
|- ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) ) |
168 |
167 126
|
eqtr3d |
|- ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) = ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) ) |
169 |
144 151 168
|
3brtr3d |
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( vol* o. H ) ) ~~> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) ) |