Metamath Proof Explorer

Theorem ddemeas

Description: The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018)

Ref Expression
Assertion ddemeas 
|- Ddelta e. ( measures ` ~P RR )

Proof

Step Hyp Ref Expression
1 1xr 
 |-  1 e. RR*
2 0le1 
 |-  0 <_ 1
3 pnfge 
 |-  ( 1 e. RR* -> 1 <_ +oo )
4 1 3 ax-mp 
 |-  1 <_ +oo
5 0xr 
 |-  0 e. RR*
6 pnfxr 
 |-  +oo e. RR*
7 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( 1 e. ( 0 [,] +oo ) <-> ( 1 e. RR* /\ 0 <_ 1 /\ 1 <_ +oo ) ) )
8 5 6 7 mp2an 
 |-  ( 1 e. ( 0 [,] +oo ) <-> ( 1 e. RR* /\ 0 <_ 1 /\ 1 <_ +oo ) )
9 1 2 4 8 mpbir3an 
 |-  1 e. ( 0 [,] +oo )
10 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
11 9 10 ifcli 
 |-  if ( 0 e. a , 1 , 0 ) e. ( 0 [,] +oo )
12 11 rgenw 
 |-  A. a e. ~P RR if ( 0 e. a , 1 , 0 ) e. ( 0 [,] +oo )
13 df-dde 
 |-  Ddelta = ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )
14 13 fmpt 
 |-  ( A. a e. ~P RR if ( 0 e. a , 1 , 0 ) e. ( 0 [,] +oo ) <-> Ddelta : ~P RR --> ( 0 [,] +oo ) )
15 12 14 mpbi 
 |-  Ddelta : ~P RR --> ( 0 [,] +oo )
16 0ss 
 |-  (/) C_ RR
17 noel 
 |-  -. 0 e. (/)
18 ddeval0 
 |-  ( ( (/) C_ RR /\ -. 0 e. (/) ) -> ( Ddelta ` (/) ) = 0 )
19 16 17 18 mp2an 
 |-  ( Ddelta ` (/) ) = 0
20 rabxm 
 |-  x = ( { a e. x | 0 e. a } u. { a e. x | -. 0 e. a } )
21 esumeq1 
 |-  ( x = ( { a e. x | 0 e. a } u. { a e. x | -. 0 e. a } ) -> sum* y e. x ( Ddelta ` y ) = sum* y e. ( { a e. x | 0 e. a } u. { a e. x | -. 0 e. a } ) ( Ddelta ` y ) )
22 20 21 ax-mp 
 |-  sum* y e. x ( Ddelta ` y ) = sum* y e. ( { a e. x | 0 e. a } u. { a e. x | -. 0 e. a } ) ( Ddelta ` y )
23 nfv 
 |-  F/ y x e. ~P ~P RR
24 nfcv 
 |-  F/_ y { a e. x | 0 e. a }
25 nfcv 
 |-  F/_ y { a e. x | -. 0 e. a }
26 rabexg 
 |-  ( x e. ~P ~P RR -> { a e. x | 0 e. a } e. _V )
27 rabexg 
 |-  ( x e. ~P ~P RR -> { a e. x | -. 0 e. a } e. _V )
28 rabnc 
 |-  ( { a e. x | 0 e. a } i^i { a e. x | -. 0 e. a } ) = (/)
29 28 a1i 
 |-  ( x e. ~P ~P RR -> ( { a e. x | 0 e. a } i^i { a e. x | -. 0 e. a } ) = (/) )
30 elrabi 
 |-  ( y e. { a e. x | 0 e. a } -> y e. x )
31 30 adantl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | 0 e. a } ) -> y e. x )
32 simpl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | 0 e. a } ) -> x e. ~P ~P RR )
33 elelpwi 
 |-  ( ( y e. x /\ x e. ~P ~P RR ) -> y e. ~P RR )
34 31 32 33 syl2anc 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | 0 e. a } ) -> y e. ~P RR )
35 15 ffvelrni 
 |-  ( y e. ~P RR -> ( Ddelta ` y ) e. ( 0 [,] +oo ) )
36 34 35 syl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | 0 e. a } ) -> ( Ddelta ` y ) e. ( 0 [,] +oo ) )
37 elrabi 
 |-  ( y e. { a e. x | -. 0 e. a } -> y e. x )
38 37 adantl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> y e. x )
39 simpl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> x e. ~P ~P RR )
40 38 39 33 syl2anc 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> y e. ~P RR )
41 40 35 syl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> ( Ddelta ` y ) e. ( 0 [,] +oo ) )
42 23 24 25 26 27 29 36 41 esumsplit 
 |-  ( x e. ~P ~P RR -> sum* y e. ( { a e. x | 0 e. a } u. { a e. x | -. 0 e. a } ) ( Ddelta ` y ) = ( sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) +e sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) ) )
43 22 42 syl5eq 
 |-  ( x e. ~P ~P RR -> sum* y e. x ( Ddelta ` y ) = ( sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) +e sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) ) )
44 43 adantr 
 |-  ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) -> sum* y e. x ( Ddelta ` y ) = ( sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) +e sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) ) )
45 esumeq1 
 |-  ( { a e. x | 0 e. a } = { k } -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = sum* y e. { k } ( Ddelta ` y ) )
46 45 adantl 
 |-  ( ( ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) /\ k e. x ) /\ { a e. x | 0 e. a } = { k } ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = sum* y e. { k } ( Ddelta ` y ) )
47 simp-4l 
 |-  ( ( ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) /\ k e. x ) /\ { a e. x | 0 e. a } = { k } ) -> x e. ~P ~P RR )
48 vex 
 |-  k e. _V
49 48 rabsnel 
 |-  ( { a e. x | 0 e. a } = { k } -> k e. x )
50 49 adantl 
 |-  ( ( ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) /\ k e. x ) /\ { a e. x | 0 e. a } = { k } ) -> k e. x )
51 eleq2w 
 |-  ( a = k -> ( 0 e. a <-> 0 e. k ) )
52 48 51 rabsnt 
 |-  ( { a e. x | 0 e. a } = { k } -> 0 e. k )
53 52 adantl 
 |-  ( ( ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) /\ k e. x ) /\ { a e. x | 0 e. a } = { k } ) -> 0 e. k )
54 elelpwi 
 |-  ( ( k e. x /\ x e. ~P ~P RR ) -> k e. ~P RR )
55 54 ancoms 
 |-  ( ( x e. ~P ~P RR /\ k e. x ) -> k e. ~P RR )
56 55 adantrr 
 |-  ( ( x e. ~P ~P RR /\ ( k e. x /\ 0 e. k ) ) -> k e. ~P RR )
57 simpr 
 |-  ( ( k e. ~P RR /\ y = k ) -> y = k )
58 57 fveq2d 
 |-  ( ( k e. ~P RR /\ y = k ) -> ( Ddelta ` y ) = ( Ddelta ` k ) )
59 48 a1i 
 |-  ( k e. ~P RR -> k e. _V )
60 15 ffvelrni 
 |-  ( k e. ~P RR -> ( Ddelta ` k ) e. ( 0 [,] +oo ) )
61 58 59 60 esumsn 
 |-  ( k e. ~P RR -> sum* y e. { k } ( Ddelta ` y ) = ( Ddelta ` k ) )
62 56 61 syl 
 |-  ( ( x e. ~P ~P RR /\ ( k e. x /\ 0 e. k ) ) -> sum* y e. { k } ( Ddelta ` y ) = ( Ddelta ` k ) )
63 56 elpwid 
 |-  ( ( x e. ~P ~P RR /\ ( k e. x /\ 0 e. k ) ) -> k C_ RR )
64 simprr 
 |-  ( ( x e. ~P ~P RR /\ ( k e. x /\ 0 e. k ) ) -> 0 e. k )
65 ddeval1 
 |-  ( ( k C_ RR /\ 0 e. k ) -> ( Ddelta ` k ) = 1 )
66 63 64 65 syl2anc 
 |-  ( ( x e. ~P ~P RR /\ ( k e. x /\ 0 e. k ) ) -> ( Ddelta ` k ) = 1 )
67 62 66 eqtrd 
 |-  ( ( x e. ~P ~P RR /\ ( k e. x /\ 0 e. k ) ) -> sum* y e. { k } ( Ddelta ` y ) = 1 )
68 47 50 53 67 syl12anc 
 |-  ( ( ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) /\ k e. x ) /\ { a e. x | 0 e. a } = { k } ) -> sum* y e. { k } ( Ddelta ` y ) = 1 )
69 46 68 eqtrd 
 |-  ( ( ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) /\ k e. x ) /\ { a e. x | 0 e. a } = { k } ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = 1 )
70 df-disj 
 |-  ( Disj_ y e. x y <-> A. k E* y e. x k e. y )
71 c0ex 
 |-  0 e. _V
72 eleq1 
 |-  ( k = 0 -> ( k e. y <-> 0 e. y ) )
73 72 rmobidv 
 |-  ( k = 0 -> ( E* y e. x k e. y <-> E* y e. x 0 e. y ) )
74 71 73 spcv 
 |-  ( A. k E* y e. x k e. y -> E* y e. x 0 e. y )
75 70 74 sylbi 
 |-  ( Disj_ y e. x y -> E* y e. x 0 e. y )
76 rmo5 
 |-  ( E* y e. x 0 e. y <-> ( E. y e. x 0 e. y -> E! y e. x 0 e. y ) )
77 76 biimpi 
 |-  ( E* y e. x 0 e. y -> ( E. y e. x 0 e. y -> E! y e. x 0 e. y ) )
78 77 imp 
 |-  ( ( E* y e. x 0 e. y /\ E. y e. x 0 e. y ) -> E! y e. x 0 e. y )
79 75 78 sylan 
 |-  ( ( Disj_ y e. x y /\ E. y e. x 0 e. y ) -> E! y e. x 0 e. y )
80 reusn 
 |-  ( E! y e. x 0 e. y <-> E. k { y e. x | 0 e. y } = { k } )
81 79 80 sylib 
 |-  ( ( Disj_ y e. x y /\ E. y e. x 0 e. y ) -> E. k { y e. x | 0 e. y } = { k } )
82 eleq2w 
 |-  ( a = y -> ( 0 e. a <-> 0 e. y ) )
83 82 cbvrabv 
 |-  { a e. x | 0 e. a } = { y e. x | 0 e. y }
84 83 eqeq1i 
 |-  ( { a e. x | 0 e. a } = { k } <-> { y e. x | 0 e. y } = { k } )
85 49 ancri 
 |-  ( { a e. x | 0 e. a } = { k } -> ( k e. x /\ { a e. x | 0 e. a } = { k } ) )
86 84 85 sylbir 
 |-  ( { y e. x | 0 e. y } = { k } -> ( k e. x /\ { a e. x | 0 e. a } = { k } ) )
87 86 eximi 
 |-  ( E. k { y e. x | 0 e. y } = { k } -> E. k ( k e. x /\ { a e. x | 0 e. a } = { k } ) )
88 df-rex 
 |-  ( E. k e. x { a e. x | 0 e. a } = { k } <-> E. k ( k e. x /\ { a e. x | 0 e. a } = { k } ) )
89 87 88 sylibr 
 |-  ( E. k { y e. x | 0 e. y } = { k } -> E. k e. x { a e. x | 0 e. a } = { k } )
90 81 89 syl 
 |-  ( ( Disj_ y e. x y /\ E. y e. x 0 e. y ) -> E. k e. x { a e. x | 0 e. a } = { k } )
91 90 adantll 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) -> E. k e. x { a e. x | 0 e. a } = { k } )
92 69 91 r19.29a 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = 1 )
93 elpwi 
 |-  ( x e. ~P ~P RR -> x C_ ~P RR )
94 sspwuni 
 |-  ( x C_ ~P RR <-> U. x C_ RR )
95 93 94 sylib 
 |-  ( x e. ~P ~P RR -> U. x C_ RR )
96 eluni2 
 |-  ( 0 e. U. x <-> E. y e. x 0 e. y )
97 96 biimpri 
 |-  ( E. y e. x 0 e. y -> 0 e. U. x )
98 ddeval1 
 |-  ( ( U. x C_ RR /\ 0 e. U. x ) -> ( Ddelta ` U. x ) = 1 )
99 95 97 98 syl2an 
 |-  ( ( x e. ~P ~P RR /\ E. y e. x 0 e. y ) -> ( Ddelta ` U. x ) = 1 )
100 99 adantlr 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) -> ( Ddelta ` U. x ) = 1 )
101 92 100 eqtr4d 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ E. y e. x 0 e. y ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = ( Ddelta ` U. x ) )
102 nfre1 
 |-  F/ y E. y e. x 0 e. y
103 102 nfn 
 |-  F/ y -. E. y e. x 0 e. y
104 82 elrab 
 |-  ( y e. { a e. x | 0 e. a } <-> ( y e. x /\ 0 e. y ) )
105 104 exbii 
 |-  ( E. y y e. { a e. x | 0 e. a } <-> E. y ( y e. x /\ 0 e. y ) )
106 neq0 
 |-  ( -. { a e. x | 0 e. a } = (/) <-> E. y y e. { a e. x | 0 e. a } )
107 df-rex 
 |-  ( E. y e. x 0 e. y <-> E. y ( y e. x /\ 0 e. y ) )
108 105 106 107 3bitr4i 
 |-  ( -. { a e. x | 0 e. a } = (/) <-> E. y e. x 0 e. y )
109 108 biimpi 
 |-  ( -. { a e. x | 0 e. a } = (/) -> E. y e. x 0 e. y )
110 109 con1i 
 |-  ( -. E. y e. x 0 e. y -> { a e. x | 0 e. a } = (/) )
111 103 110 esumeq1d 
 |-  ( -. E. y e. x 0 e. y -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = sum* y e. (/) ( Ddelta ` y ) )
112 esumnul 
 |-  sum* y e. (/) ( Ddelta ` y ) = 0
113 111 112 eqtrdi 
 |-  ( -. E. y e. x 0 e. y -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = 0 )
114 113 adantl 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ -. E. y e. x 0 e. y ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = 0 )
115 96 biimpi 
 |-  ( 0 e. U. x -> E. y e. x 0 e. y )
116 115 con3i 
 |-  ( -. E. y e. x 0 e. y -> -. 0 e. U. x )
117 ddeval0 
 |-  ( ( U. x C_ RR /\ -. 0 e. U. x ) -> ( Ddelta ` U. x ) = 0 )
118 95 116 117 syl2an 
 |-  ( ( x e. ~P ~P RR /\ -. E. y e. x 0 e. y ) -> ( Ddelta ` U. x ) = 0 )
119 118 adantlr 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ -. E. y e. x 0 e. y ) -> ( Ddelta ` U. x ) = 0 )
120 114 119 eqtr4d 
 |-  ( ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) /\ -. E. y e. x 0 e. y ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = ( Ddelta ` U. x ) )
121 101 120 pm2.61dan 
 |-  ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) -> sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) = ( Ddelta ` U. x ) )
122 40 elpwid 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> y C_ RR )
123 82 notbid 
 |-  ( a = y -> ( -. 0 e. a <-> -. 0 e. y ) )
124 123 elrab 
 |-  ( y e. { a e. x | -. 0 e. a } <-> ( y e. x /\ -. 0 e. y ) )
125 124 simprbi 
 |-  ( y e. { a e. x | -. 0 e. a } -> -. 0 e. y )
126 125 adantl 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> -. 0 e. y )
127 ddeval0 
 |-  ( ( y C_ RR /\ -. 0 e. y ) -> ( Ddelta ` y ) = 0 )
128 122 126 127 syl2anc 
 |-  ( ( x e. ~P ~P RR /\ y e. { a e. x | -. 0 e. a } ) -> ( Ddelta ` y ) = 0 )
129 128 esumeq2dv 
 |-  ( x e. ~P ~P RR -> sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) = sum* y e. { a e. x | -. 0 e. a } 0 )
130 vex 
 |-  x e. _V
131 130 rabex 
 |-  { a e. x | -. 0 e. a } e. _V
132 25 esum0 
 |-  ( { a e. x | -. 0 e. a } e. _V -> sum* y e. { a e. x | -. 0 e. a } 0 = 0 )
133 131 132 ax-mp 
 |-  sum* y e. { a e. x | -. 0 e. a } 0 = 0
134 129 133 eqtrdi 
 |-  ( x e. ~P ~P RR -> sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) = 0 )
135 134 adantr 
 |-  ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) -> sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) = 0 )
136 121 135 oveq12d 
 |-  ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) -> ( sum* y e. { a e. x | 0 e. a } ( Ddelta ` y ) +e sum* y e. { a e. x | -. 0 e. a } ( Ddelta ` y ) ) = ( ( Ddelta ` U. x ) +e 0 ) )
137 vuniex 
 |-  U. x e. _V
138 137 elpw 
 |-  ( U. x e. ~P RR <-> U. x C_ RR )
139 138 biimpri 
 |-  ( U. x C_ RR -> U. x e. ~P RR )
140 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
141 15 ffvelrni 
 |-  ( U. x e. ~P RR -> ( Ddelta ` U. x ) e. ( 0 [,] +oo ) )
142 140 141 sseldi 
 |-  ( U. x e. ~P RR -> ( Ddelta ` U. x ) e. RR* )
143 xaddid1 
 |-  ( ( Ddelta ` U. x ) e. RR* -> ( ( Ddelta ` U. x ) +e 0 ) = ( Ddelta ` U. x ) )
144 95 139 142 143 4syl 
 |-  ( x e. ~P ~P RR -> ( ( Ddelta ` U. x ) +e 0 ) = ( Ddelta ` U. x ) )
145 144 adantr 
 |-  ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) -> ( ( Ddelta ` U. x ) +e 0 ) = ( Ddelta ` U. x ) )
146 44 136 145 3eqtrrd 
 |-  ( ( x e. ~P ~P RR /\ Disj_ y e. x y ) -> ( Ddelta ` U. x ) = sum* y e. x ( Ddelta ` y ) )
147 146 adantrl 
 |-  ( ( x e. ~P ~P RR /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( Ddelta ` U. x ) = sum* y e. x ( Ddelta ` y ) )
148 147 ex 
 |-  ( x e. ~P ~P RR -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( Ddelta ` U. x ) = sum* y e. x ( Ddelta ` y ) ) )
149 148 rgen 
 |-  A. x e. ~P ~P RR ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( Ddelta ` U. x ) = sum* y e. x ( Ddelta ` y ) )
150 reex 
 |-  RR e. _V
151 pwsiga 
 |-  ( RR e. _V -> ~P RR e. ( sigAlgebra ` RR ) )
152 150 151 ax-mp 
 |-  ~P RR e. ( sigAlgebra ` RR )
153 elrnsiga 
 |-  ( ~P RR e. ( sigAlgebra ` RR ) -> ~P RR e. U. ran sigAlgebra )
154 ismeas 
 |-  ( ~P RR e. U. ran sigAlgebra -> ( Ddelta e. ( measures ` ~P RR ) <-> ( Ddelta : ~P RR --> ( 0 [,] +oo ) /\ ( Ddelta ` (/) ) = 0 /\ A. x e. ~P ~P RR ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( Ddelta ` U. x ) = sum* y e. x ( Ddelta ` y ) ) ) ) )
155 152 153 154 mp2b 
 |-  ( Ddelta e. ( measures ` ~P RR ) <-> ( Ddelta : ~P RR --> ( 0 [,] +oo ) /\ ( Ddelta ` (/) ) = 0 /\ A. x e. ~P ~P RR ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( Ddelta ` U. x ) = sum* y e. x ( Ddelta ` y ) ) ) )
156 15 19 149 155 mpbir3an 
 |-  Ddelta e. ( measures ` ~P RR )