Metamath Proof Explorer

Theorem uniioombllem2

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by Mario Carneiro, 11-Dec-2016) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses uniioombl.1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2 
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
uniioombl.a 
|- A = U. ran ( (,) o. F )
uniioombl.e 
|- ( ph -> ( vol* ` E ) e. RR )
uniioombl.c 
|- ( ph -> C e. RR+ )
uniioombl.g 
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s 
|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v 
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
uniioombllem2.h 
|- H = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
uniioombllem2.k 
|- K = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
Assertion uniioombllem2 
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( vol* o. H ) ) ~~> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) )

Proof

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 sseldi 
 |-  ( ( 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 sseldi 
 |-  ( ( ( 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 syl5eq 
 |-  ( ( 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 ) ) )