Metamath Proof Explorer

Theorem ovolval3

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

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

Proof

Step Hyp Ref Expression
1 ovolval3.a 
 |-  ( ph -> A C_ RR )
2 ovolval3.m 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol 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 = ( sum^ ` ( ( abs o. - ) o. f ) ) ) } = { 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 ) ) ) }
4 1 3 ovolval2 
 |-  ( ph -> ( vol* ` A ) = inf ( { 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 ) ) ) } , RR* , < ) )
5 reex 
 |-  RR e. _V
6 5 5 xpex 
 |-  ( RR X. RR ) e. _V
7 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
8 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 ) )
9 6 7 8 mp2an 
 |-  ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN )
10 9 sseli 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f e. ( ( RR X. RR ) ^m NN ) )
11 elmapi 
 |-  ( f e. ( ( RR X. RR ) ^m NN ) -> f : NN --> ( RR X. RR ) )
12 10 11 syl 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( RR X. RR ) )
13 12 ffvelrnda 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( f ` n ) e. ( RR X. RR ) )
14 1st2nd2 
 |-  ( ( f ` n ) e. ( RR X. RR ) -> ( f ` n ) = <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. )
15 13 14 syl 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( f ` n ) = <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. )
16 15 fveq2d 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( (,) ` ( f ` n ) ) = ( (,) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. ) )
17 df-ov 
 |-  ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) = ( (,) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. )
18 17 eqcomi 
 |-  ( (,) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. ) = ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) )
19 18 a1i 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( (,) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. ) = ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) )
20 16 19 eqtrd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( (,) ` ( f ` n ) ) = ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) )
21 20 fveq2d 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( vol ` ( (,) ` ( f ` n ) ) ) = ( vol ` ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) ) )
22 xp1st 
 |-  ( ( f ` n ) e. ( RR X. RR ) -> ( 1st ` ( f ` n ) ) e. RR )
23 13 22 syl 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( 1st ` ( f ` n ) ) e. RR )
24 xp2nd 
 |-  ( ( f ` n ) e. ( RR X. RR ) -> ( 2nd ` ( f ` n ) ) e. RR )
25 13 24 syl 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( 2nd ` ( f ` n ) ) e. RR )
26 elmapi 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
27 26 adantr 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
28 simpr 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> n e. NN )
29 ovolfcl 
 |-  ( ( f : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( f ` n ) ) e. RR /\ ( 2nd ` ( f ` n ) ) e. RR /\ ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) )
30 27 28 29 syl2anc 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( 1st ` ( f ` n ) ) e. RR /\ ( 2nd ` ( f ` n ) ) e. RR /\ ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) )
31 30 simp3d 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) )
32 volioo 
 |-  ( ( ( 1st ` ( f ` n ) ) e. RR /\ ( 2nd ` ( f ` n ) ) e. RR /\ ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) -> ( vol ` ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) ) = ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) )
33 23 25 31 32 syl3anc 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( vol ` ( ( 1st ` ( f ` n ) ) (,) ( 2nd ` ( f ` n ) ) ) ) = ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) )
34 21 33 eqtrd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( vol ` ( (,) ` ( f ` n ) ) ) = ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) )
35 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
36 ffun 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
37 35 36 ax-mp 
 |-  Fun (,)
38 37 a1i 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> Fun (,) )
39 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
40 39 13 sseldi 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( f ` n ) e. ( RR* X. RR* ) )
41 35 fdmi 
 |-  dom (,) = ( RR* X. RR* )
42 41 eqcomi 
 |-  ( RR* X. RR* ) = dom (,)
43 42 a1i 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( RR* X. RR* ) = dom (,) )
44 40 43 eleqtrd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( f ` n ) e. dom (,) )
45 fvco 
 |-  ( ( Fun (,) /\ ( f ` n ) e. dom (,) ) -> ( ( vol o. (,) ) ` ( f ` n ) ) = ( vol ` ( (,) ` ( f ` n ) ) ) )
46 38 44 45 syl2anc 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( vol o. (,) ) ` ( f ` n ) ) = ( vol ` ( (,) ` ( f ` n ) ) ) )
47 15 fveq2d 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( abs o. - ) ` ( f ` n ) ) = ( ( abs o. - ) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. ) )
48 df-ov 
 |-  ( ( 1st ` ( f ` n ) ) ( abs o. - ) ( 2nd ` ( f ` n ) ) ) = ( ( abs o. - ) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. )
49 48 eqcomi 
 |-  ( ( abs o. - ) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. ) = ( ( 1st ` ( f ` n ) ) ( abs o. - ) ( 2nd ` ( f ` n ) ) )
50 49 a1i 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( abs o. - ) ` <. ( 1st ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) >. ) = ( ( 1st ` ( f ` n ) ) ( abs o. - ) ( 2nd ` ( f ` n ) ) ) )
51 23 recnd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( 1st ` ( f ` n ) ) e. CC )
52 25 recnd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( 2nd ` ( f ` n ) ) e. CC )
53 eqid 
 |-  ( abs o. - ) = ( abs o. - )
54 53 cnmetdval 
 |-  ( ( ( 1st ` ( f ` n ) ) e. CC /\ ( 2nd ` ( f ` n ) ) e. CC ) -> ( ( 1st ` ( f ` n ) ) ( abs o. - ) ( 2nd ` ( f ` n ) ) ) = ( abs ` ( ( 1st ` ( f ` n ) ) - ( 2nd ` ( f ` n ) ) ) ) )
55 51 52 54 syl2anc 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( 1st ` ( f ` n ) ) ( abs o. - ) ( 2nd ` ( f ` n ) ) ) = ( abs ` ( ( 1st ` ( f ` n ) ) - ( 2nd ` ( f ` n ) ) ) ) )
56 abssub 
 |-  ( ( ( 1st ` ( f ` n ) ) e. CC /\ ( 2nd ` ( f ` n ) ) e. CC ) -> ( abs ` ( ( 1st ` ( f ` n ) ) - ( 2nd ` ( f ` n ) ) ) ) = ( abs ` ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) ) )
57 51 52 56 syl2anc 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( abs ` ( ( 1st ` ( f ` n ) ) - ( 2nd ` ( f ` n ) ) ) ) = ( abs ` ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) ) )
58 23 25 31 abssubge0d 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( abs ` ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) ) = ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) )
59 55 57 58 3eqtrd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( 1st ` ( f ` n ) ) ( abs o. - ) ( 2nd ` ( f ` n ) ) ) = ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) )
60 47 50 59 3eqtrd 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( abs o. - ) ` ( f ` n ) ) = ( ( 2nd ` ( f ` n ) ) - ( 1st ` ( f ` n ) ) ) )
61 34 46 60 3eqtr4d 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ n e. NN ) -> ( ( vol o. (,) ) ` ( f ` n ) ) = ( ( abs o. - ) ` ( f ` n ) ) )
62 61 mpteq2dva 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( n e. NN |-> ( ( vol o. (,) ) ` ( f ` n ) ) ) = ( n e. NN |-> ( ( abs o. - ) ` ( f ` n ) ) ) )
63 volioof 
 |-  ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )
64 63 a1i 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) )
65 39 a1i 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( RR X. RR ) C_ ( RR* X. RR* ) )
66 12 65 fssd 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( RR* X. RR* ) )
67 fcompt 
 |-  ( ( ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo ) /\ f : NN --> ( RR* X. RR* ) ) -> ( ( vol o. (,) ) o. f ) = ( n e. NN |-> ( ( vol o. (,) ) ` ( f ` n ) ) ) )
68 64 66 67 syl2anc 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( ( vol o. (,) ) o. f ) = ( n e. NN |-> ( ( vol o. (,) ) ` ( f ` n ) ) ) )
69 absf 
 |-  abs : CC --> RR
70 subf 
 |-  - : ( CC X. CC ) --> CC
71 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
72 69 70 71 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
73 72 a1i 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
74 rr2sscn2 
 |-  ( RR X. RR ) C_ ( CC X. CC )
75 74 a1i 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( RR X. RR ) C_ ( CC X. CC ) )
76 12 75 fssd 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> f : NN --> ( CC X. CC ) )
77 fcompt 
 |-  ( ( ( abs o. - ) : ( CC X. CC ) --> RR /\ f : NN --> ( CC X. CC ) ) -> ( ( abs o. - ) o. f ) = ( n e. NN |-> ( ( abs o. - ) ` ( f ` n ) ) ) )
78 73 76 77 syl2anc 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( ( abs o. - ) o. f ) = ( n e. NN |-> ( ( abs o. - ) ` ( f ` n ) ) ) )
79 62 68 78 3eqtr4d 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( ( vol o. (,) ) o. f ) = ( ( abs o. - ) o. f ) )
80 79 fveq2d 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( sum^ ` ( ( vol o. (,) ) o. f ) ) = ( sum^ ` ( ( abs o. - ) o. f ) ) )
81 80 eqeq2d 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) <-> y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) )
82 81 anbi2d 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) ) )
83 82 rexbiia 
 |-  ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( abs o. - ) o. f ) ) ) )
84 83 rabbii 
 |-  { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) } = { 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 ) ) ) }
85 2 84 eqtr2i 
 |-  { 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
86 85 infeq1i 
 |-  inf ( { 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 ) ) ) } , RR* , < ) = inf ( M , RR* , < )
87 86 a1i 
 |-  ( ph -> inf ( { 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 ) ) ) } , RR* , < ) = inf ( M , RR* , < ) )
88 4 87 eqtrd 
 |-  ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )