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

Theorem omsmeas 32590
Description: The restriction of a constructed outer measure to Caratheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020.)
Hypotheses
Ref Expression
omsmeas.m 𝑀 = (toOMeas‘𝑅)
omsmeas.s 𝑆 = (toCaraSiga‘𝑀)
omsmeas.o (𝜑𝑄𝑉)
omsmeas.r (𝜑𝑅:𝑄⟶(0[,]+∞))
omsmeas.d (𝜑 → ∅ ∈ dom 𝑅)
omsmeas.0 (𝜑 → (𝑅‘∅) = 0)
Assertion
Ref Expression
omsmeas (𝜑 → (𝑀𝑆) ∈ (measures‘𝑆))

Proof of Theorem omsmeas
Dummy variables 𝑒 𝑓 𝑥 𝑦 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omsmeas.o . . . . . 6 (𝜑𝑄𝑉)
2 omsmeas.r . . . . . 6 (𝜑𝑅:𝑄⟶(0[,]+∞))
3 omsf 32563 . . . . . 6 ((𝑄𝑉𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
41, 2, 3syl2anc 584 . . . . 5 (𝜑 → (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞))
5 omsmeas.m . . . . . . 7 𝑀 = (toOMeas‘𝑅)
65a1i 11 . . . . . 6 (𝜑𝑀 = (toOMeas‘𝑅))
72fdmd 6663 . . . . . . . . 9 (𝜑 → dom 𝑅 = 𝑄)
87eqcomd 2742 . . . . . . . 8 (𝜑𝑄 = dom 𝑅)
98unieqd 4867 . . . . . . 7 (𝜑 𝑄 = dom 𝑅)
109pweqd 4565 . . . . . 6 (𝜑 → 𝒫 𝑄 = 𝒫 dom 𝑅)
116, 10feq12d 6640 . . . . 5 (𝜑 → (𝑀:𝒫 𝑄⟶(0[,]+∞) ↔ (toOMeas‘𝑅):𝒫 dom 𝑅⟶(0[,]+∞)))
124, 11mpbird 256 . . . 4 (𝜑𝑀:𝒫 𝑄⟶(0[,]+∞))
13 omsmeas.s . . . . 5 𝑆 = (toCaraSiga‘𝑀)
141uniexd 7658 . . . . . 6 (𝜑 𝑄 ∈ V)
1514, 12carsgcl 32571 . . . . 5 (𝜑 → (toCaraSiga‘𝑀) ⊆ 𝒫 𝑄)
1613, 15eqsstrid 3980 . . . 4 (𝜑𝑆 ⊆ 𝒫 𝑄)
1712, 16fssresd 6693 . . 3 (𝜑 → (𝑀𝑆):𝑆⟶(0[,]+∞))
18 omsmeas.d . . . . . . . 8 (𝜑 → ∅ ∈ dom 𝑅)
19 omsmeas.0 . . . . . . . 8 (𝜑 → (𝑅‘∅) = 0)
205, 1, 2, 18, 19oms0 32564 . . . . . . 7 (𝜑 → (𝑀‘∅) = 0)
2114, 12, 200elcarsg 32574 . . . . . 6 (𝜑 → ∅ ∈ (toCaraSiga‘𝑀))
2221, 13eleqtrrdi 2848 . . . . 5 (𝜑 → ∅ ∈ 𝑆)
23 fvres 6845 . . . . 5 (∅ ∈ 𝑆 → ((𝑀𝑆)‘∅) = (𝑀‘∅))
2422, 23syl 17 . . . 4 (𝜑 → ((𝑀𝑆)‘∅) = (𝑀‘∅))
2524, 20eqtrd 2776 . . 3 (𝜑 → ((𝑀𝑆)‘∅) = 0)
26 nfcv 2904 . . . . . . . 8 𝑔𝑓
27 nfcv 2904 . . . . . . . 8 𝑓𝑔
28 id 22 . . . . . . . 8 (𝑓 = 𝑔𝑓 = 𝑔)
2926, 27, 28cbvdisj 5068 . . . . . . 7 (Disj 𝑓𝑒 𝑓Disj 𝑔𝑒 𝑔)
3029anbi2i 623 . . . . . 6 ((𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓) ↔ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔))
311ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑄𝑉)
322ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑅:𝑄⟶(0[,]+∞))
33 simplr 766 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒 ∈ 𝒫 𝑆)
3433elpwid 4557 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒𝑆)
3516ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑆 ⊆ 𝒫 𝑄)
3634, 35sstrd 3942 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒 ⊆ 𝒫 𝑄)
3736sselda 3932 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → 𝑓 ∈ 𝒫 𝑄)
3837elpwid 4557 . . . . . . . . . 10 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → 𝑓 𝑄)
39 simprl 768 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒 ≼ ω)
405, 31, 32, 38, 39omssubadd 32567 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (𝑀 𝑓𝑒 𝑓) ≤ Σ*𝑓𝑒(𝑀𝑓))
4114ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑄 ∈ V)
4212ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑀:𝒫 𝑄⟶(0[,]+∞))
4320ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (𝑀‘∅) = 0)
44 uniiun 5006 . . . . . . . . . . . . . . . 16 𝑥 = 𝑦𝑥 𝑦
4544fveq2i 6829 . . . . . . . . . . . . . . 15 (𝑀 𝑥) = (𝑀 𝑦𝑥 𝑦)
4613ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → 𝑄𝑉)
4723ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → 𝑅:𝑄⟶(0[,]+∞))
48 simpl3 1192 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) ∧ 𝑦𝑥) → 𝑥 ⊆ 𝒫 𝑄)
49 simpr 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) ∧ 𝑦𝑥) → 𝑦𝑥)
5048, 49sseldd 3933 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) ∧ 𝑦𝑥) → 𝑦 ∈ 𝒫 𝑄)
5150elpwid 4557 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) ∧ 𝑦𝑥) → 𝑦 𝑄)
52 simp2 1136 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → 𝑥 ≼ ω)
535, 46, 47, 51, 52omssubadd 32567 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → (𝑀 𝑦𝑥 𝑦) ≤ Σ*𝑦𝑥(𝑀𝑦))
5445, 53eqbrtrid 5128 . . . . . . . . . . . . . 14 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
55543adant1r 1176 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
56553adant1r 1176 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑄) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
5713ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑄) → 𝑄𝑉)
5823ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑄) → 𝑅:𝑄⟶(0[,]+∞))
59 simp2 1136 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑄) → 𝑥𝑦)
60 elpwi 4555 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝒫 𝑄𝑦 𝑄)
61603ad2ant3 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑄) → 𝑦 𝑄)
625, 57, 58, 59, 61omsmon 32565 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑄) → (𝑀𝑥) ≤ (𝑀𝑦))
63623adant1r 1176 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑄) → (𝑀𝑥) ≤ (𝑀𝑦))
64633adant1r 1176 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑄) → (𝑀𝑥) ≤ (𝑀𝑦))
65 elpwi 4555 . . . . . . . . . . . . . 14 (𝑒 ∈ 𝒫 𝑆𝑒𝑆)
6665ad2antlr 724 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒𝑆)
6766, 13sseqtrdi 3982 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒 ⊆ (toCaraSiga‘𝑀))
6841, 42, 43, 56, 64, 39, 67carsgclctun 32588 . . . . . . . . . . 11 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒 ∈ (toCaraSiga‘𝑀))
6968, 13eleqtrrdi 2848 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → 𝑒𝑆)
70 fvres 6845 . . . . . . . . . . 11 ( 𝑒𝑆 → ((𝑀𝑆)‘ 𝑒) = (𝑀 𝑒))
71 uniiun 5006 . . . . . . . . . . . 12 𝑒 = 𝑓𝑒 𝑓
7271fveq2i 6829 . . . . . . . . . . 11 (𝑀 𝑒) = (𝑀 𝑓𝑒 𝑓)
7370, 72eqtrdi 2792 . . . . . . . . . 10 ( 𝑒𝑆 → ((𝑀𝑆)‘ 𝑒) = (𝑀 𝑓𝑒 𝑓))
7469, 73syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ((𝑀𝑆)‘ 𝑒) = (𝑀 𝑓𝑒 𝑓))
75 nfv 1916 . . . . . . . . . 10 𝑓((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔))
7666sselda 3932 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → 𝑓𝑆)
77 fvres 6845 . . . . . . . . . . . 12 (𝑓𝑆 → ((𝑀𝑆)‘𝑓) = (𝑀𝑓))
7876, 77syl 17 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → ((𝑀𝑆)‘𝑓) = (𝑀𝑓))
7978ralrimiva 3139 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ∀𝑓𝑒 ((𝑀𝑆)‘𝑓) = (𝑀𝑓))
8075, 79esumeq2d 32303 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓𝑒((𝑀𝑆)‘𝑓) = Σ*𝑓𝑒(𝑀𝑓))
8140, 74, 803brtr4d 5125 . . . . . . . 8 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ((𝑀𝑆)‘ 𝑒) ≤ Σ*𝑓𝑒((𝑀𝑆)‘𝑓))
82 snex 5377 . . . . . . . . . . . . 13 {∅} ∈ V
8382a1i 11 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → {∅} ∈ V)
8442adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → 𝑀:𝒫 𝑄⟶(0[,]+∞))
8584, 37ffvelcdmd 7019 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → (𝑀𝑓) ∈ (0[,]+∞))
86 elsni 4591 . . . . . . . . . . . . . 14 (𝑓 ∈ {∅} → 𝑓 = ∅)
8786fveq2d 6830 . . . . . . . . . . . . 13 (𝑓 ∈ {∅} → (𝑀𝑓) = (𝑀‘∅))
8887, 43sylan9eqr 2798 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓 ∈ {∅}) → (𝑀𝑓) = 0)
8933, 83, 85, 88esumpad2 32322 . . . . . . . . . . 11 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓 ∈ (𝑒 ∖ {∅})(𝑀𝑓) = Σ*𝑓𝑒(𝑀𝑓))
90 neldifsnd 4741 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ¬ ∅ ∈ (𝑒 ∖ {∅}))
91 difss 4079 . . . . . . . . . . . . . 14 (𝑒 ∖ {∅}) ⊆ 𝑒
92 ssdomg 8862 . . . . . . . . . . . . . 14 (𝑒 ∈ 𝒫 𝑆 → ((𝑒 ∖ {∅}) ⊆ 𝑒 → (𝑒 ∖ {∅}) ≼ 𝑒))
9333, 91, 92mpisyl 21 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (𝑒 ∖ {∅}) ≼ 𝑒)
94 domtr 8869 . . . . . . . . . . . . 13 (((𝑒 ∖ {∅}) ≼ 𝑒𝑒 ≼ ω) → (𝑒 ∖ {∅}) ≼ ω)
9593, 39, 94syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (𝑒 ∖ {∅}) ≼ ω)
9667ssdifssd 4090 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (𝑒 ∖ {∅}) ⊆ (toCaraSiga‘𝑀))
97 simprr 770 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Disj 𝑔𝑒 𝑔)
98 nfcv 2904 . . . . . . . . . . . . . . 15 𝑦𝑔
99 nfcv 2904 . . . . . . . . . . . . . . 15 𝑔𝑦
100 id 22 . . . . . . . . . . . . . . 15 (𝑔 = 𝑦𝑔 = 𝑦)
10198, 99, 100cbvdisj 5068 . . . . . . . . . . . . . 14 (Disj 𝑔𝑒 𝑔Disj 𝑦𝑒 𝑦)
10297, 101sylib 217 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Disj 𝑦𝑒 𝑦)
103 disjss1 5064 . . . . . . . . . . . . 13 ((𝑒 ∖ {∅}) ⊆ 𝑒 → (Disj 𝑦𝑒 𝑦Disj 𝑦 ∈ (𝑒 ∖ {∅})𝑦))
10491, 102, 103mpsyl 68 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Disj 𝑦 ∈ (𝑒 ∖ {∅})𝑦)
10541, 42, 43, 56, 90, 95, 96, 104, 64carsggect 32585 . . . . . . . . . . 11 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓 ∈ (𝑒 ∖ {∅})(𝑀𝑓) ≤ (𝑀 (𝑒 ∖ {∅})))
10689, 105eqbrtrrd 5117 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓𝑒(𝑀𝑓) ≤ (𝑀 (𝑒 ∖ {∅})))
107 unidif0 5303 . . . . . . . . . . 11 (𝑒 ∖ {∅}) = 𝑒
108107fveq2i 6829 . . . . . . . . . 10 (𝑀 (𝑒 ∖ {∅})) = (𝑀 𝑒)
109106, 108breqtrdi 5134 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓𝑒(𝑀𝑓) ≤ (𝑀 𝑒))
11069, 70syl 17 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ((𝑀𝑆)‘ 𝑒) = (𝑀 𝑒))
111109, 80, 1103brtr4d 5125 . . . . . . . 8 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ≤ ((𝑀𝑆)‘ 𝑒))
11281, 111jca 512 . . . . . . 7 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (((𝑀𝑆)‘ 𝑒) ≤ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∧ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ≤ ((𝑀𝑆)‘ 𝑒)))
113 iccssxr 13264 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
11417ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (𝑀𝑆):𝑆⟶(0[,]+∞))
115114, 69ffvelcdmd 7019 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ((𝑀𝑆)‘ 𝑒) ∈ (0[,]+∞))
116113, 115sselid 3930 . . . . . . . 8 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ((𝑀𝑆)‘ 𝑒) ∈ ℝ*)
117114adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → (𝑀𝑆):𝑆⟶(0[,]+∞))
118117, 76ffvelcdmd 7019 . . . . . . . . . . 11 ((((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) ∧ 𝑓𝑒) → ((𝑀𝑆)‘𝑓) ∈ (0[,]+∞))
119118ralrimiva 3139 . . . . . . . . . 10 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ∀𝑓𝑒 ((𝑀𝑆)‘𝑓) ∈ (0[,]+∞))
120 nfcv 2904 . . . . . . . . . . 11 𝑓𝑒
121120esumcl 32296 . . . . . . . . . 10 ((𝑒 ∈ 𝒫 𝑆 ∧ ∀𝑓𝑒 ((𝑀𝑆)‘𝑓) ∈ (0[,]+∞)) → Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∈ (0[,]+∞))
12233, 119, 121syl2anc 584 . . . . . . . . 9 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∈ (0[,]+∞))
123113, 122sselid 3930 . . . . . . . 8 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∈ ℝ*)
124 xrletri3 12990 . . . . . . . 8 ((((𝑀𝑆)‘ 𝑒) ∈ ℝ* ∧ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∈ ℝ*) → (((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ↔ (((𝑀𝑆)‘ 𝑒) ≤ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∧ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ≤ ((𝑀𝑆)‘ 𝑒))))
125116, 123, 124syl2anc 584 . . . . . . 7 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → (((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ↔ (((𝑀𝑆)‘ 𝑒) ≤ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ∧ Σ*𝑓𝑒((𝑀𝑆)‘𝑓) ≤ ((𝑀𝑆)‘ 𝑒))))
126112, 125mpbird 256 . . . . . 6 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑔𝑒 𝑔)) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓))
12730, 126sylan2b 594 . . . . 5 (((𝜑𝑒 ∈ 𝒫 𝑆) ∧ (𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓)) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓))
128127ex 413 . . . 4 ((𝜑𝑒 ∈ 𝒫 𝑆) → ((𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓)))
129128ralrimiva 3139 . . 3 (𝜑 → ∀𝑒 ∈ 𝒫 𝑆((𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓)))
13017, 25, 1293jca 1127 . 2 (𝜑 → ((𝑀𝑆):𝑆⟶(0[,]+∞) ∧ ((𝑀𝑆)‘∅) = 0 ∧ ∀𝑒 ∈ 𝒫 𝑆((𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓))))
13114, 12, 20, 54, 62carsgsiga 32589 . . . 4 (𝜑 → (toCaraSiga‘𝑀) ∈ (sigAlgebra‘ 𝑄))
13213, 131eqeltrid 2841 . . 3 (𝜑𝑆 ∈ (sigAlgebra‘ 𝑄))
133 elrnsiga 32392 . . 3 (𝑆 ∈ (sigAlgebra‘ 𝑄) → 𝑆 ran sigAlgebra)
134 ismeas 32465 . . 3 (𝑆 ran sigAlgebra → ((𝑀𝑆) ∈ (measures‘𝑆) ↔ ((𝑀𝑆):𝑆⟶(0[,]+∞) ∧ ((𝑀𝑆)‘∅) = 0 ∧ ∀𝑒 ∈ 𝒫 𝑆((𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓)))))
135132, 133, 1343syl 18 . 2 (𝜑 → ((𝑀𝑆) ∈ (measures‘𝑆) ↔ ((𝑀𝑆):𝑆⟶(0[,]+∞) ∧ ((𝑀𝑆)‘∅) = 0 ∧ ∀𝑒 ∈ 𝒫 𝑆((𝑒 ≼ ω ∧ Disj 𝑓𝑒 𝑓) → ((𝑀𝑆)‘ 𝑒) = Σ*𝑓𝑒((𝑀𝑆)‘𝑓)))))
136130, 135mpbird 256 1 (𝜑 → (𝑀𝑆) ∈ (measures‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wral 3061  Vcvv 3441  cdif 3895  wss 3898  c0 4270  𝒫 cpw 4548  {csn 4574   cuni 4853   ciun 4942  Disj wdisj 5058   class class class wbr 5093  dom cdm 5621  ran crn 5622  cres 5623  wf 6476  cfv 6480  (class class class)co 7338  ωcom 7781  cdom 8803  0cc0 10973  +∞cpnf 11108  *cxr 11110  cle 11112  [,]cicc 13184  Σ*cesum 32293  sigAlgebracsiga 32374  measurescmeas 32461  toOMeascoms 32558  toCaraSigaccarsg 32568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-reg 9450  ax-inf2 9499  ax-cc 10293  ax-ac2 10321  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051  ax-addf 11052  ax-mulf 11053
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-disj 5059  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-of 7596  df-om 7782  df-1st 7900  df-2nd 7901  df-supp 8049  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-2o 8369  df-oadd 8372  df-er 8570  df-map 8689  df-pm 8690  df-ixp 8758  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fsupp 9228  df-fi 9269  df-sup 9300  df-inf 9301  df-oi 9368  df-r1 9622  df-rank 9623  df-dju 9759  df-card 9797  df-acn 9800  df-ac 9974  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-xnn0 12408  df-z 12422  df-dec 12540  df-uz 12685  df-q 12791  df-rp 12833  df-xneg 12950  df-xadd 12951  df-xmul 12952  df-ioo 13185  df-ioc 13186  df-ico 13187  df-icc 13188  df-fz 13342  df-fzo 13485  df-fl 13614  df-mod 13692  df-seq 13824  df-exp 13885  df-fac 14090  df-bc 14119  df-hash 14147  df-shft 14878  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-sum 15498  df-ef 15877  df-sin 15879  df-cos 15880  df-pi 15882  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-ordt 17310  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-ps 18382  df-tsr 18383  df-plusf 18423  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-mhm 18528  df-submnd 18529  df-grp 18677  df-minusg 18678  df-sbg 18679  df-mulg 18798  df-subg 18849  df-cntz 19020  df-cmn 19484  df-abl 19485  df-mgp 19817  df-ur 19834  df-ring 19881  df-cring 19882  df-subrg 20128  df-abv 20184  df-lmod 20232  df-scaf 20233  df-sra 20541  df-rgmod 20542  df-psmet 20696  df-xmet 20697  df-met 20698  df-bl 20699  df-mopn 20700  df-fbas 20701  df-fg 20702  df-cnfld 20705  df-top 22150  df-topon 22167  df-topsp 22189  df-bases 22203  df-cld 22277  df-ntr 22278  df-cls 22279  df-nei 22356  df-lp 22394  df-perf 22395  df-cn 22485  df-cnp 22486  df-haus 22573  df-tx 22820  df-hmeo 23013  df-fil 23104  df-fm 23196  df-flim 23197  df-flf 23198  df-tmd 23330  df-tgp 23331  df-tsms 23385  df-trg 23418  df-xms 23580  df-ms 23581  df-tms 23582  df-nm 23845  df-ngp 23846  df-nrg 23848  df-nlm 23849  df-ii 24147  df-cncf 24148  df-limc 25137  df-dv 25138  df-log 25819  df-esum 32294  df-siga 32375  df-meas 32462  df-oms 32559  df-carsg 32569
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator