Metamath Proof Explorer

Theorem ovolval2

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ . See ovolval for an alternative expression. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval2.a 
|- ( ph -> A C_ RR )
ovolval2.m 
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) }
Assertion ovolval2 
|- ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovolval2.a 
 |-  ( ph -> A C_ RR )
2 ovolval2.m 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) }
3 eqid 
 |-  { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
4 3 ovolval 
 |-  ( A C_ RR -> ( vol* ` A ) = inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
5 1 4 syl 
 |-  ( ph -> ( vol* ` A ) = inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) )
6 3 a1i 
 |-  ( ph -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } )
7 reex 
 |-  RR e. _V
8 7 7 xpex 
 |-  ( RR X. RR ) e. _V
9 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
10 mapss 
 |-  ( ( ( RR X. RR ) e. _V /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN ) )
11 8 9 10 mp2an 
 |-  ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN )
12 11 sseli 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f e. ( ( RR X. RR ) ^m NN ) )
13 1zzd 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> 1 e. ZZ )
14 12 13 syl 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> 1 e. ZZ )
15 14 adantl 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> 1 e. ZZ )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 absfico 
 |-  abs : CC --> ( 0 [,) +oo )
18 subf 
 |-  - : ( CC X. CC ) --> CC
19 fco 
 |-  ( ( abs : CC --> ( 0 [,) +oo ) /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> ( 0 [,) +oo ) )
20 17 18 19 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> ( 0 [,) +oo )
21 20 a1i 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( abs o. - ) : ( CC X. CC ) --> ( 0 [,) +oo ) )
22 rr2sscn2 
 |-  ( RR X. RR ) C_ ( CC X. CC )
23 22 a1i 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( RR X. RR ) C_ ( CC X. CC ) )
24 elmapi 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR X. RR ) )
25 12 24 syl 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( RR X. RR ) )
26 21 23 25 fcoss 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( ( abs o. - ) o. f ) : NN --> ( 0 [,) +oo ) )
27 26 adantl 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( abs o. - ) o. f ) : NN --> ( 0 [,) +oo ) )
28 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
29 15 16 27 28 sge0seq 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( sum^ ` ( ( abs o. - ) o. f ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
30 29 eqcomd 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) = ( sum^ ` ( ( abs o. - ) o. f ) ) )
31 30 eqeq2d 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <-> y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) )
32 31 anbi2d 
 |-  ( ( ph /\ f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ) -> ( ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) ) )
33 32 rexbidva 
 |-  ( ph -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) ) )
34 33 rabbidv 
 |-  ( ph -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) } )
35 2 eqcomi 
 |-  { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) } = M
36 35 a1i 
 |-  ( ph -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) } = M )
37 6 34 36 3eqtrd 
 |-  ( ph -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = M )
38 37 infeq1d 
 |-  ( ph -> inf ( { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } , RR* , < ) = inf ( M , RR* , < ) )
39 5 38 eqtrd 
 |-  ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )