Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismeannd Structured version   Visualization version   GIF version

Theorem ismeannd 45262
Description: Sufficient condition to prove that 𝑀 is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
ismeannd.sal (𝜑𝑆 ∈ SAlg)
ismeannd.mf (𝜑𝑀:𝑆⟶(0[,]+∞))
ismeannd.m0 (𝜑 → (𝑀‘∅) = 0)
ismeannd.iun ((𝜑𝑒:ℕ⟶𝑆Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑛 ∈ ℕ (𝑒𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))))
Assertion
Ref Expression
ismeannd (𝜑𝑀 ∈ Meas)
Distinct variable groups:   𝑒,𝑀,𝑛   𝜑,𝑒,𝑛
Allowed substitution hints:   𝑆(𝑒,𝑛)

Proof of Theorem ismeannd
Dummy variables 𝑥 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ismeannd.mf . . . . 5 (𝜑𝑀:𝑆⟶(0[,]+∞))
21fdmd 6728 . . . . . 6 (𝜑 → dom 𝑀 = 𝑆)
32feq2d 6703 . . . . 5 (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ↔ 𝑀:𝑆⟶(0[,]+∞)))
41, 3mpbird 256 . . . 4 (𝜑𝑀:dom 𝑀⟶(0[,]+∞))
5 ismeannd.sal . . . . 5 (𝜑𝑆 ∈ SAlg)
62, 5eqeltrd 2833 . . . 4 (𝜑 → dom 𝑀 ∈ SAlg)
74, 6jca 512 . . 3 (𝜑 → (𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg))
8 ismeannd.m0 . . 3 (𝜑 → (𝑀‘∅) = 0)
9 unieq 4919 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
10 uni0 4939 . . . . . . . . . . . . 13 ∅ = ∅
1110a1i 11 . . . . . . . . . . . 12 (𝑥 = ∅ → ∅ = ∅)
129, 11eqtrd 2772 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
1312fveq2d 6895 . . . . . . . . . 10 (𝑥 = ∅ → (𝑀 𝑥) = (𝑀‘∅))
1413, 8sylan9eqr 2794 . . . . . . . . 9 ((𝜑𝑥 = ∅) → (𝑀 𝑥) = 0)
15 reseq2 5976 . . . . . . . . . . . . 13 (𝑥 = ∅ → (𝑀𝑥) = (𝑀 ↾ ∅))
16 res0 5985 . . . . . . . . . . . . . 14 (𝑀 ↾ ∅) = ∅
1716a1i 11 . . . . . . . . . . . . 13 (𝑥 = ∅ → (𝑀 ↾ ∅) = ∅)
1815, 17eqtrd 2772 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑀𝑥) = ∅)
1918fveq2d 6895 . . . . . . . . . . 11 (𝑥 = ∅ → (Σ^‘(𝑀𝑥)) = (Σ^‘∅))
2019adantl 482 . . . . . . . . . 10 ((𝜑𝑥 = ∅) → (Σ^‘(𝑀𝑥)) = (Σ^‘∅))
21 sge00 45171 . . . . . . . . . . 11 ^‘∅) = 0
2221a1i 11 . . . . . . . . . 10 ((𝜑𝑥 = ∅) → (Σ^‘∅) = 0)
2320, 22eqtrd 2772 . . . . . . . . 9 ((𝜑𝑥 = ∅) → (Σ^‘(𝑀𝑥)) = 0)
2414, 23eqtr4d 2775 . . . . . . . 8 ((𝜑𝑥 = ∅) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
2524adantlr 713 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑥 = ∅) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
2625adantlr 713 . . . . . 6 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 = ∅) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
27 simpll 765 . . . . . . . 8 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → (𝜑𝑥 ∈ 𝒫 dom 𝑀))
28 simplrr 776 . . . . . . . 8 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → Disj 𝑦𝑥 𝑦)
2927, 28jca 512 . . . . . . 7 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → ((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦))
30 simplrl 775 . . . . . . . 8 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → 𝑥 ≼ ω)
31 neqne 2948 . . . . . . . . 9 𝑥 = ∅ → 𝑥 ≠ ∅)
3231adantl 482 . . . . . . . 8 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → 𝑥 ≠ ∅)
33 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑤𝑦 = 𝑤)
3433cbvdisjv 5124 . . . . . . . . . . 11 (Disj 𝑦𝑥 𝑦Disj 𝑤𝑥 𝑤)
3534biimpi 215 . . . . . . . . . 10 (Disj 𝑦𝑥 𝑦Disj 𝑤𝑥 𝑤)
3635adantl 482 . . . . . . . . 9 ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → Disj 𝑤𝑥 𝑤)
3736ad2antlr 725 . . . . . . . 8 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → Disj 𝑤𝑥 𝑤)
3830, 32, 37nnfoctbdj 45251 . . . . . . 7 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → ∃𝑒(𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)))
39 simpl 483 . . . . . . . . . 10 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛))) → ((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦))
40 simprl 769 . . . . . . . . . 10 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛))) → 𝑒:ℕ–onto→(𝑥 ∪ {∅}))
41 simprr 771 . . . . . . . . . 10 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛))) → Disj 𝑛 ∈ ℕ (𝑒𝑛))
42 founiiun0 43968 . . . . . . . . . . . . 13 (𝑒:ℕ–onto→(𝑥 ∪ {∅}) → 𝑥 = 𝑛 ∈ ℕ (𝑒𝑛))
4342fveq2d 6895 . . . . . . . . . . . 12 (𝑒:ℕ–onto→(𝑥 ∪ {∅}) → (𝑀 𝑥) = (𝑀 𝑛 ∈ ℕ (𝑒𝑛)))
4443ad2antlr 725 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑥) = (𝑀 𝑛 ∈ ℕ (𝑒𝑛)))
45 simplll 773 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → 𝜑)
46 fof 6805 . . . . . . . . . . . . . . . 16 (𝑒:ℕ–onto→(𝑥 ∪ {∅}) → 𝑒:ℕ⟶(𝑥 ∪ {∅}))
4746adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) → 𝑒:ℕ⟶(𝑥 ∪ {∅}))
48 elpwi 4609 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ 𝒫 dom 𝑀𝑥 ⊆ dom 𝑀)
4948adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → 𝑥 ⊆ dom 𝑀)
502adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → dom 𝑀 = 𝑆)
5149, 50sseqtrd 4022 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → 𝑥𝑆)
52 0sal 45115 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ SAlg → ∅ ∈ 𝑆)
535, 52syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∅ ∈ 𝑆)
54 snssi 4811 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ 𝑆 → {∅} ⊆ 𝑆)
5553, 54syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → {∅} ⊆ 𝑆)
5655adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → {∅} ⊆ 𝑆)
5751, 56unssd 4186 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (𝑥 ∪ {∅}) ⊆ 𝑆)
5857adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) → (𝑥 ∪ {∅}) ⊆ 𝑆)
5947, 58fssd 6735 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) → 𝑒:ℕ⟶𝑆)
6059adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → 𝑒:ℕ⟶𝑆)
61 simpr 485 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → Disj 𝑛 ∈ ℕ (𝑒𝑛))
62 ismeannd.iun . . . . . . . . . . . . 13 ((𝜑𝑒:ℕ⟶𝑆Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑛 ∈ ℕ (𝑒𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))))
6345, 60, 61, 62syl3anc 1371 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑛 ∈ ℕ (𝑒𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))))
6463adantllr 717 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑛 ∈ ℕ (𝑒𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))))
651feqmptd 6960 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 = (𝑦𝑆 ↦ (𝑀𝑦)))
6665reseq1d 5980 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀𝑥) = ((𝑦𝑆 ↦ (𝑀𝑦)) ↾ 𝑥))
6766adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (𝑀𝑥) = ((𝑦𝑆 ↦ (𝑀𝑦)) ↾ 𝑥))
6867adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (𝑀𝑥) = ((𝑦𝑆 ↦ (𝑀𝑦)) ↾ 𝑥))
6951resmptd 6040 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → ((𝑦𝑆 ↦ (𝑀𝑦)) ↾ 𝑥) = (𝑦𝑥 ↦ (𝑀𝑦)))
7069adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → ((𝑦𝑆 ↦ (𝑀𝑦)) ↾ 𝑥) = (𝑦𝑥 ↦ (𝑀𝑦)))
71 snssi 4811 . . . . . . . . . . . . . . . . . . . . 21 (∅ ∈ 𝑥 → {∅} ⊆ 𝑥)
72 ssequn2 4183 . . . . . . . . . . . . . . . . . . . . 21 ({∅} ⊆ 𝑥 ↔ (𝑥 ∪ {∅}) = 𝑥)
7371, 72sylib 217 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ 𝑥 → (𝑥 ∪ {∅}) = 𝑥)
7473eqcomd 2738 . . . . . . . . . . . . . . . . . . 19 (∅ ∈ 𝑥𝑥 = (𝑥 ∪ {∅}))
7574mpteq1d 5243 . . . . . . . . . . . . . . . . . 18 (∅ ∈ 𝑥 → (𝑦𝑥 ↦ (𝑀𝑦)) = (𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦)))
7675adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (𝑦𝑥 ↦ (𝑀𝑦)) = (𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦)))
7768, 70, 763eqtrd 2776 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (𝑀𝑥) = (𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦)))
7877fveq2d 6895 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ∅ ∈ 𝑥) → (Σ^‘(𝑀𝑥)) = (Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦))))
79 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑦((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥)
80 simplr 767 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → 𝑥 ∈ 𝒫 dom 𝑀)
81 p0ex 5382 . . . . . . . . . . . . . . . . . 18 {∅} ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → {∅} ∈ V)
83 disjsn 4715 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∩ {∅}) = ∅ ↔ ¬ ∅ ∈ 𝑥)
8483biimpri 227 . . . . . . . . . . . . . . . . . 18 (¬ ∅ ∈ 𝑥 → (𝑥 ∩ {∅}) = ∅)
8584adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → (𝑥 ∩ {∅}) = ∅)
861ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦𝑥) → 𝑀:𝑆⟶(0[,]+∞))
8751sselda 3982 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦𝑥) → 𝑦𝑆)
8886, 87ffvelcdmd 7087 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦𝑥) → (𝑀𝑦) ∈ (0[,]+∞))
8988adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) ∧ 𝑦𝑥) → (𝑀𝑦) ∈ (0[,]+∞))
90 elsni 4645 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {∅} → 𝑦 = ∅)
9190fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {∅} → (𝑀𝑦) = (𝑀‘∅))
9291adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ {∅}) → (𝑀𝑦) = (𝑀‘∅))
931, 53ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀‘∅) ∈ (0[,]+∞))
9493adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ {∅}) → (𝑀‘∅) ∈ (0[,]+∞))
9592, 94eqeltrd 2833 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ {∅}) → (𝑀𝑦) ∈ (0[,]+∞))
9695ad4ant14 750 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) ∧ 𝑦 ∈ {∅}) → (𝑀𝑦) ∈ (0[,]+∞))
9779, 80, 82, 85, 89, 96sge0splitmpt 45206 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → (Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦))) = ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒^‘(𝑦 ∈ {∅} ↦ (𝑀𝑦)))))
98 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ∅ → (𝑀𝑦) = (𝑀‘∅))
9998adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 = ∅) → (𝑀𝑦) = (𝑀‘∅))
1008adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 = ∅) → (𝑀‘∅) = 0)
10199, 100eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 = ∅) → (𝑀𝑦) = 0)
10290, 101sylan2 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ {∅}) → (𝑀𝑦) = 0)
103102mpteq2dva 5248 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑦 ∈ {∅} ↦ (𝑀𝑦)) = (𝑦 ∈ {∅} ↦ 0))
104103fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Σ^‘(𝑦 ∈ {∅} ↦ (𝑀𝑦))) = (Σ^‘(𝑦 ∈ {∅} ↦ 0)))
105 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑦𝜑
10681a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {∅} ∈ V)
107105, 106sge0z 45170 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (Σ^‘(𝑦 ∈ {∅} ↦ 0)) = 0)
108104, 107eqtrd 2772 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Σ^‘(𝑦 ∈ {∅} ↦ (𝑀𝑦))) = 0)
109108oveq2d 7427 . . . . . . . . . . . . . . . . 17 (𝜑 → ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒^‘(𝑦 ∈ {∅} ↦ (𝑀𝑦)))) = ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒 0))
110109ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒^‘(𝑦 ∈ {∅} ↦ (𝑀𝑦)))) = ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒 0))
111 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → 𝑥 ∈ 𝒫 dom 𝑀)
11267, 69eqtrd 2772 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (𝑀𝑥) = (𝑦𝑥 ↦ (𝑀𝑦)))
1131adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → 𝑀:𝑆⟶(0[,]+∞))
114113, 51fssresd 6758 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (𝑀𝑥):𝑥⟶(0[,]+∞))
115112, 114feq1dd 43945 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (𝑦𝑥 ↦ (𝑀𝑦)):𝑥⟶(0[,]+∞))
116111, 115sge0xrcl 45180 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) ∈ ℝ*)
117116xaddridd 13224 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒 0) = (Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))))
118112fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (Σ^‘(𝑀𝑥)) = (Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))))
119118eqcomd 2738 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) = (Σ^‘(𝑀𝑥)))
120117, 119eqtrd 2772 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒 0) = (Σ^‘(𝑀𝑥)))
121120adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → ((Σ^‘(𝑦𝑥 ↦ (𝑀𝑦))) +𝑒 0) = (Σ^‘(𝑀𝑥)))
12297, 110, 1213eqtrrd 2777 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ ¬ ∅ ∈ 𝑥) → (Σ^‘(𝑀𝑥)) = (Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦))))
12378, 122pm2.61dan 811 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → (Σ^‘(𝑀𝑥)) = (Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦))))
124123ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (Σ^‘(𝑀𝑥)) = (Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦))))
125 nfv 1917 . . . . . . . . . . . . . 14 𝑦(((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛))
126 nfv 1917 . . . . . . . . . . . . . . 15 𝑛((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅}))
127 nfdisj1 5127 . . . . . . . . . . . . . . 15 𝑛Disj 𝑛 ∈ ℕ (𝑒𝑛)
128126, 127nfan 1902 . . . . . . . . . . . . . 14 𝑛(((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛))
129 fveq2 6891 . . . . . . . . . . . . . 14 (𝑦 = (𝑒𝑛) → (𝑀𝑦) = (𝑀‘(𝑒𝑛)))
130 nnex 12220 . . . . . . . . . . . . . . 15 ℕ ∈ V
131130a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → ℕ ∈ V)
132 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → 𝑒:ℕ–onto→(𝑥 ∪ {∅}))
133 eqidd 2733 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) ∧ 𝑛 ∈ ℕ) → (𝑒𝑛) = (𝑒𝑛))
1341ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → 𝑀:𝑆⟶(0[,]+∞))
13557sselda 3982 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → 𝑦𝑆)
136134, 135ffvelcdmd 7087 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → (𝑀𝑦) ∈ (0[,]+∞))
137136ad4ant14 750 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) ∧ 𝑦 ∈ (𝑥 ∪ {∅})) → (𝑀𝑦) ∈ (0[,]+∞))
13845, 101sylan 580 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) ∧ 𝑦 = ∅) → (𝑀𝑦) = 0)
139125, 128, 129, 131, 132, 61, 133, 137, 138sge0fodjrn 45212 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (Σ^‘(𝑦 ∈ (𝑥 ∪ {∅}) ↦ (𝑀𝑦))) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))))
140124, 139eqtr2d 2773 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))) = (Σ^‘(𝑀𝑥)))
141140adantllr 717 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒𝑛)))) = (Σ^‘(𝑀𝑥)))
14244, 64, 1413eqtrd 2776 . . . . . . . . . 10 (((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ 𝑒:ℕ–onto→(𝑥 ∪ {∅})) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
14339, 40, 41, 142syl21anc 836 . . . . . . . . 9 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) ∧ (𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛))) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
144143ex 413 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) → ((𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥))))
145144exlimdv 1936 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ Disj 𝑦𝑥 𝑦) → (∃𝑒(𝑒:ℕ–onto→(𝑥 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑒𝑛)) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥))))
14629, 38, 145sylc 65 . . . . . 6 ((((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ¬ 𝑥 = ∅) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
14726, 146pm2.61dan 811 . . . . 5 (((𝜑𝑥 ∈ 𝒫 dom 𝑀) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))
148147ex 413 . . . 4 ((𝜑𝑥 ∈ 𝒫 dom 𝑀) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥))))
149148ralrimiva 3146 . . 3 (𝜑 → ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥))))
1507, 8, 149jca31 515 . 2 (𝜑 → (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))))
151 ismea 45246 . 2 (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (𝑀 𝑥) = (Σ^‘(𝑀𝑥)))))
152150, 151sylibr 233 1 (𝜑𝑀 ∈ Meas)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2940  wral 3061  Vcvv 3474  cun 3946  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602  {csn 4628   cuni 4908   ciun 4997  Disj wdisj 5113   class class class wbr 5148  cmpt 5231  dom cdm 5676  cres 5678  wf 6539  ontowfo 6541  cfv 6543  (class class class)co 7411  ωcom 7857  cdom 8939  0cc0 11112  +∞cpnf 11247  cn 12214   +𝑒 cxad 13092  [,]cicc 13329  SAlgcsalg 45103  Σ^csumge0 45157  Meascmea 45244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-xadd 13095  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-sum 15635  df-salg 45104  df-sumge0 45158  df-mea 45245
This theorem is referenced by:  volmea  45269  caratheodory  45323
  Copyright terms: Public domain W3C validator