Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  measres Structured version   Visualization version   GIF version

Theorem measres 29612
Description: Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
Assertion
Ref Expression
measres ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → (𝑀𝑇) ∈ (measures‘𝑇))

Proof of Theorem measres
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1055 . 2 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → 𝑇 ran sigAlgebra)
2 measfrge0 29593 . . . . 5 (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞))
323ad2ant1 1075 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → 𝑀:𝑆⟶(0[,]+∞))
4 simp3 1056 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → 𝑇𝑆)
53, 4fssresd 5984 . . 3 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → (𝑀𝑇):𝑇⟶(0[,]+∞))
6 0elsiga 29504 . . . . 5 (𝑇 ran sigAlgebra → ∅ ∈ 𝑇)
7 fvres 6117 . . . . 5 (∅ ∈ 𝑇 → ((𝑀𝑇)‘∅) = (𝑀‘∅))
81, 6, 73syl 18 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → ((𝑀𝑇)‘∅) = (𝑀‘∅))
9 measvnul 29596 . . . . 5 (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
1093ad2ant1 1075 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → (𝑀‘∅) = 0)
118, 10eqtrd 2644 . . 3 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → ((𝑀𝑇)‘∅) = 0)
12 simp11 1084 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑀 ∈ (measures‘𝑆))
13 simp13 1086 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑇𝑆)
14 simp2 1055 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑇)
15 sspwb 4844 . . . . . . . . 9 (𝑇𝑆 ↔ 𝒫 𝑇 ⊆ 𝒫 𝑆)
16 ssel2 3563 . . . . . . . . 9 ((𝒫 𝑇 ⊆ 𝒫 𝑆𝑥 ∈ 𝒫 𝑇) → 𝑥 ∈ 𝒫 𝑆)
1715, 16sylanb 488 . . . . . . . 8 ((𝑇𝑆𝑥 ∈ 𝒫 𝑇) → 𝑥 ∈ 𝒫 𝑆)
1813, 14, 17syl2anc 691 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ∈ 𝒫 𝑆)
19 simp3 1056 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
20 measvun 29599 . . . . . . 7 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑥 ∈ 𝒫 𝑆 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑀 𝑥) = Σ*𝑦𝑥(𝑀𝑦))
2112, 18, 19, 20syl3anc 1318 . . . . . 6 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑀 𝑥) = Σ*𝑦𝑥(𝑀𝑦))
2213ad2ant1 1075 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑇 ran sigAlgebra)
23 simp3l 1082 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 ≼ ω)
24 sigaclcu 29507 . . . . . . . 8 ((𝑇 ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇𝑥 ≼ ω) → 𝑥𝑇)
2522, 14, 23, 24syl3anc 1318 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥𝑇)
26 fvres 6117 . . . . . . 7 ( 𝑥𝑇 → ((𝑀𝑇)‘ 𝑥) = (𝑀 𝑥))
2725, 26syl 17 . . . . . 6 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → ((𝑀𝑇)‘ 𝑥) = (𝑀 𝑥))
28 elpwi 4117 . . . . . . . . . . 11 (𝑥 ∈ 𝒫 𝑇𝑥𝑇)
2928sselda 3568 . . . . . . . . . 10 ((𝑥 ∈ 𝒫 𝑇𝑦𝑥) → 𝑦𝑇)
3029adantll 746 . . . . . . . . 9 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) ∧ 𝑦𝑥) → 𝑦𝑇)
31 fvres 6117 . . . . . . . . 9 (𝑦𝑇 → ((𝑀𝑇)‘𝑦) = (𝑀𝑦))
3230, 31syl 17 . . . . . . . 8 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) ∧ 𝑦𝑥) → ((𝑀𝑇)‘𝑦) = (𝑀𝑦))
3332esumeq2dv 29427 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) → Σ*𝑦𝑥((𝑀𝑇)‘𝑦) = Σ*𝑦𝑥(𝑀𝑦))
34333adant3 1074 . . . . . 6 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → Σ*𝑦𝑥((𝑀𝑇)‘𝑦) = Σ*𝑦𝑥(𝑀𝑦))
3521, 27, 343eqtr4d 2654 . . . . 5 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → ((𝑀𝑇)‘ 𝑥) = Σ*𝑦𝑥((𝑀𝑇)‘𝑦))
36353expia 1259 . . . 4 (((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) ∧ 𝑥 ∈ 𝒫 𝑇) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → ((𝑀𝑇)‘ 𝑥) = Σ*𝑦𝑥((𝑀𝑇)‘𝑦)))
3736ralrimiva 2949 . . 3 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → ((𝑀𝑇)‘ 𝑥) = Σ*𝑦𝑥((𝑀𝑇)‘𝑦)))
385, 11, 373jca 1235 . 2 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → ((𝑀𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → ((𝑀𝑇)‘ 𝑥) = Σ*𝑦𝑥((𝑀𝑇)‘𝑦))))
39 ismeas 29589 . . 3 (𝑇 ran sigAlgebra → ((𝑀𝑇) ∈ (measures‘𝑇) ↔ ((𝑀𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → ((𝑀𝑇)‘ 𝑥) = Σ*𝑦𝑥((𝑀𝑇)‘𝑦)))))
4039biimprd 237 . 2 (𝑇 ran sigAlgebra → (((𝑀𝑇):𝑇⟶(0[,]+∞) ∧ ((𝑀𝑇)‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑇((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → ((𝑀𝑇)‘ 𝑥) = Σ*𝑦𝑥((𝑀𝑇)‘𝑦))) → (𝑀𝑇) ∈ (measures‘𝑇)))
411, 38, 40sylc 63 1 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ran sigAlgebra ∧ 𝑇𝑆) → (𝑀𝑇) ∈ (measures‘𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031   = wceq 1475  wcel 1977  wral 2896  wss 3540  c0 3874  𝒫 cpw 4108   cuni 4372  Disj wdisj 4553   class class class wbr 4583  ran crn 5039  cres 5040  wf 5800  cfv 5804  (class class class)co 6549  ωcom 6957  cdom 7839  0cc0 9815  +∞cpnf 9950  [,]cicc 12049  Σ*cesum 29416  sigAlgebracsiga 29497  measurescmeas 29585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-esum 29417  df-siga 29498  df-meas 29586
This theorem is referenced by:  measinb2  29613
  Copyright terms: Public domain W3C validator