Metamath Proof Explorer

Theorem oms0

Description: A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses oms.m 
|- M = ( toOMeas ` R )
oms.o 
|- ( ph -> Q e. V )
oms.r 
|- ( ph -> R : Q --> ( 0 [,] +oo ) )
oms.d 
|- ( ph -> (/) e. dom R )
oms.0 
|- ( ph -> ( R ` (/) ) = 0 )
Assertion oms0 
|- ( ph -> ( M ` (/) ) = 0 )

Proof

Step Hyp Ref Expression
1 oms.m 
 |-  M = ( toOMeas ` R )
2 oms.o 
 |-  ( ph -> Q e. V )
3 oms.r 
 |-  ( ph -> R : Q --> ( 0 [,] +oo ) )
4 oms.d 
 |-  ( ph -> (/) e. dom R )
5 oms.0 
 |-  ( ph -> ( R ` (/) ) = 0 )
6 1 fveq1i 
 |-  ( M ` (/) ) = ( ( toOMeas ` R ) ` (/) )
7 0ss 
 |-  (/) C_ U. dom R
8 3 fdmd 
 |-  ( ph -> dom R = Q )
9 8 unieqd 
 |-  ( ph -> U. dom R = U. Q )
10 7 9 sseqtrid 
 |-  ( ph -> (/) C_ U. Q )
11 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ (/) C_ U. Q ) -> ( ( toOMeas ` R ) ` (/) ) = inf ( ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
12 2 3 10 11 syl3anc 
 |-  ( ph -> ( ( toOMeas ` R ) ` (/) ) = inf ( ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
13 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
14 xrltso 
 |-  < Or RR*
15 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
16 13 14 15 mp2 
 |-  < Or ( 0 [,] +oo )
17 16 a1i 
 |-  ( ph -> < Or ( 0 [,] +oo ) )
18 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
19 18 a1i 
 |-  ( ph -> 0 e. ( 0 [,] +oo ) )
20 4 snssd 
 |-  ( ph -> { (/) } C_ dom R )
21 p0ex 
 |-  { (/) } e. _V
22 21 elpw 
 |-  ( { (/) } e. ~P dom R <-> { (/) } C_ dom R )
23 20 22 sylibr 
 |-  ( ph -> { (/) } e. ~P dom R )
24 0ss 
 |-  (/) C_ U. { (/) }
25 0ex 
 |-  (/) e. _V
26 snct 
 |-  ( (/) e. _V -> { (/) } ~<_ _om )
27 25 26 ax-mp 
 |-  { (/) } ~<_ _om
28 24 27 pm3.2i 
 |-  ( (/) C_ U. { (/) } /\ { (/) } ~<_ _om )
29 23 28 jctir 
 |-  ( ph -> ( { (/) } e. ~P dom R /\ ( (/) C_ U. { (/) } /\ { (/) } ~<_ _om ) ) )
30 unieq 
 |-  ( z = { (/) } -> U. z = U. { (/) } )
31 30 sseq2d 
 |-  ( z = { (/) } -> ( (/) C_ U. z <-> (/) C_ U. { (/) } ) )
32 breq1 
 |-  ( z = { (/) } -> ( z ~<_ _om <-> { (/) } ~<_ _om ) )
33 31 32 anbi12d 
 |-  ( z = { (/) } -> ( ( (/) C_ U. z /\ z ~<_ _om ) <-> ( (/) C_ U. { (/) } /\ { (/) } ~<_ _om ) ) )
34 33 elrab 
 |-  ( { (/) } e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } <-> ( { (/) } e. ~P dom R /\ ( (/) C_ U. { (/) } /\ { (/) } ~<_ _om ) ) )
35 29 34 sylibr 
 |-  ( ph -> { (/) } e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } )
36 simpr 
 |-  ( ( ph /\ y = (/) ) -> y = (/) )
37 36 fveq2d 
 |-  ( ( ph /\ y = (/) ) -> ( R ` y ) = ( R ` (/) ) )
38 5 adantr 
 |-  ( ( ph /\ y = (/) ) -> ( R ` (/) ) = 0 )
39 37 38 eqtrd 
 |-  ( ( ph /\ y = (/) ) -> ( R ` y ) = 0 )
40 39 4 19 esumsn 
 |-  ( ph -> sum* y e. { (/) } ( R ` y ) = 0 )
41 40 eqcomd 
 |-  ( ph -> 0 = sum* y e. { (/) } ( R ` y ) )
42 esumeq1 
 |-  ( x = { (/) } -> sum* y e. x ( R ` y ) = sum* y e. { (/) } ( R ` y ) )
43 42 rspceeqv 
 |-  ( ( { (/) } e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } /\ 0 = sum* y e. { (/) } ( R ` y ) ) -> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } 0 = sum* y e. x ( R ` y ) )
44 35 41 43 syl2anc 
 |-  ( ph -> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } 0 = sum* y e. x ( R ` y ) )
45 0xr 
 |-  0 e. RR*
46 eqid 
 |-  ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) = ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
47 46 elrnmpt 
 |-  ( 0 e. RR* -> ( 0 e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) <-> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } 0 = sum* y e. x ( R ` y ) ) )
48 45 47 ax-mp 
 |-  ( 0 e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) <-> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } 0 = sum* y e. x ( R ` y ) )
49 44 48 sylibr 
 |-  ( ph -> 0 e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
50 nfv 
 |-  F/ x ph
51 nfmpt1 
 |-  F/_ x ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
52 51 nfrn 
 |-  F/_ x ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
53 52 nfcri 
 |-  F/ x a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
54 50 53 nfan 
 |-  F/ x ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
55 simpr 
 |-  ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) -> a = sum* y e. x ( R ` y ) )
56 vex 
 |-  x e. _V
57 nfv 
 |-  F/ y ph
58 nfcv 
 |-  F/_ y { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) }
59 nfcv 
 |-  F/_ y x
60 59 nfesum1 
 |-  F/_ y sum* y e. x ( R ` y )
61 58 60 nfmpt 
 |-  F/_ y ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
62 61 nfrn 
 |-  F/_ y ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
63 62 nfcri 
 |-  F/ y a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
64 57 63 nfan 
 |-  F/ y ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
65 nfv 
 |-  F/ y x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) }
66 64 65 nfan 
 |-  F/ y ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } )
67 60 nfeq2 
 |-  F/ y a = sum* y e. x ( R ` y )
68 66 67 nfan 
 |-  F/ y ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) )
69 3 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> R : Q --> ( 0 [,] +oo ) )
70 ssrab2 
 |-  { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } C_ ~P dom R
71 simpllr 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } )
72 70 71 sseldi 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> x e. ~P dom R )
73 8 pweqd 
 |-  ( ph -> ~P dom R = ~P Q )
74 73 ad4antr 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> ~P dom R = ~P Q )
75 72 74 eleqtrd 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> x e. ~P Q )
76 75 elpwid 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> x C_ Q )
77 simpr 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> y e. x )
78 76 77 sseldd 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> y e. Q )
79 69 78 ffvelrnd 
 |-  ( ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) /\ y e. x ) -> ( R ` y ) e. ( 0 [,] +oo ) )
80 79 ex 
 |-  ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) -> ( y e. x -> ( R ` y ) e. ( 0 [,] +oo ) ) )
81 68 80 ralrimi 
 |-  ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) -> A. y e. x ( R ` y ) e. ( 0 [,] +oo ) )
82 59 esumcl 
 |-  ( ( x e. _V /\ A. y e. x ( R ` y ) e. ( 0 [,] +oo ) ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
83 56 81 82 sylancr 
 |-  ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
84 55 83 eqeltrd 
 |-  ( ( ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) /\ x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } ) /\ a = sum* y e. x ( R ` y ) ) -> a e. ( 0 [,] +oo ) )
85 vex 
 |-  a e. _V
86 46 elrnmpt 
 |-  ( a e. _V -> ( a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) <-> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } a = sum* y e. x ( R ` y ) ) )
87 85 86 ax-mp 
 |-  ( a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) <-> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } a = sum* y e. x ( R ` y ) )
88 87 biimpi 
 |-  ( a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) -> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } a = sum* y e. x ( R ` y ) )
89 88 adantl 
 |-  ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) -> E. x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } a = sum* y e. x ( R ` y ) )
90 54 84 89 r19.29af 
 |-  ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) -> a e. ( 0 [,] +oo ) )
91 pnfxr 
 |-  +oo e. RR*
92 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ a e. ( 0 [,] +oo ) ) -> 0 <_ a )
93 45 91 92 mp3an12 
 |-  ( a e. ( 0 [,] +oo ) -> 0 <_ a )
94 90 93 syl 
 |-  ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) -> 0 <_ a )
95 13 90 sseldi 
 |-  ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) -> a e. RR* )
96 xrlenlt 
 |-  ( ( 0 e. RR* /\ a e. RR* ) -> ( 0 <_ a <-> -. a < 0 ) )
97 96 bicomd 
 |-  ( ( 0 e. RR* /\ a e. RR* ) -> ( -. a < 0 <-> 0 <_ a ) )
98 45 95 97 sylancr 
 |-  ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) -> ( -. a < 0 <-> 0 <_ a ) )
99 94 98 mpbird 
 |-  ( ( ph /\ a e. ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) ) -> -. a < 0 )
100 17 19 49 99 infmin 
 |-  ( ph -> inf ( ran ( x e. { z e. ~P dom R | ( (/) C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) = 0 )
101 12 100 eqtrd 
 |-  ( ph -> ( ( toOMeas ` R ) ` (/) ) = 0 )
102 6 101 syl5eq 
 |-  ( ph -> ( M ` (/) ) = 0 )