Metamath Proof Explorer


Theorem ddemeas

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

Ref Expression
Assertion ddemeas δ ∈ ( measures ‘ 𝒫 ℝ )

Proof

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