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

Theorem measdivcstOLD 30635
Description: Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
measdivcstOLD ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑀   𝑥,𝑆

Proof of Theorem measdivcstOLD
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funmpt 6149 . . . . . 6 Fun (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))
2 ovex 6916 . . . . . . . 8 ((𝑀𝑥) /𝑒 𝐴) ∈ V
32rgenw 3123 . . . . . . 7 𝑥𝑆 ((𝑀𝑥) /𝑒 𝐴) ∈ V
4 dmmptg 5860 . . . . . . 7 (∀𝑥𝑆 ((𝑀𝑥) /𝑒 𝐴) ∈ V → dom (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) = 𝑆)
53, 4ax-mp 5 . . . . . 6 dom (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) = 𝑆
6 df-fn 6114 . . . . . 6 ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) Fn 𝑆 ↔ (Fun (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∧ dom (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) = 𝑆))
71, 5, 6mpbir2an 693 . . . . 5 (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) Fn 𝑆
87a1i 11 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) Fn 𝑆)
9 vex 3405 . . . . . . 7 𝑦 ∈ V
10 eqid 2817 . . . . . . . 8 (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) = (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))
1110elrnmpt 5587 . . . . . . 7 (𝑦 ∈ V → (𝑦 ∈ ran (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ↔ ∃𝑥𝑆 𝑦 = ((𝑀𝑥) /𝑒 𝐴)))
129, 11ax-mp 5 . . . . . 6 (𝑦 ∈ ran (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ↔ ∃𝑥𝑆 𝑦 = ((𝑀𝑥) /𝑒 𝐴))
13 measfrge0 30614 . . . . . . . . . . 11 (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞))
14 ffvelrn 6589 . . . . . . . . . . 11 ((𝑀:𝑆⟶(0[,]+∞) ∧ 𝑥𝑆) → (𝑀𝑥) ∈ (0[,]+∞))
1513, 14sylan 571 . . . . . . . . . 10 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑥𝑆) → (𝑀𝑥) ∈ (0[,]+∞))
1615adantlr 697 . . . . . . . . 9 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥𝑆) → (𝑀𝑥) ∈ (0[,]+∞))
17 simplr 776 . . . . . . . . 9 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥𝑆) → 𝐴 ∈ ℝ+)
1816, 17xrpxdivcld 29991 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥𝑆) → ((𝑀𝑥) /𝑒 𝐴) ∈ (0[,]+∞))
19 eleq1a 2891 . . . . . . . 8 (((𝑀𝑥) /𝑒 𝐴) ∈ (0[,]+∞) → (𝑦 = ((𝑀𝑥) /𝑒 𝐴) → 𝑦 ∈ (0[,]+∞)))
2018, 19syl 17 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑥𝑆) → (𝑦 = ((𝑀𝑥) /𝑒 𝐴) → 𝑦 ∈ (0[,]+∞)))
2120rexlimdva 3230 . . . . . 6 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (∃𝑥𝑆 𝑦 = ((𝑀𝑥) /𝑒 𝐴) → 𝑦 ∈ (0[,]+∞)))
2212, 21syl5bi 233 . . . . 5 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑦 ∈ ran (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) → 𝑦 ∈ (0[,]+∞)))
2322ssrdv 3815 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ran (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ⊆ (0[,]+∞))
24 df-f 6115 . . . 4 ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ↔ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) Fn 𝑆 ∧ ran (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ⊆ (0[,]+∞)))
258, 23, 24sylanbrc 574 . . 3 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞))
26 measbase 30608 . . . . . . . 8 (𝑀 ∈ (measures‘𝑆) → 𝑆 ran sigAlgebra)
27 0elsiga 30525 . . . . . . . 8 (𝑆 ran sigAlgebra → ∅ ∈ 𝑆)
2826, 27syl 17 . . . . . . 7 (𝑀 ∈ (measures‘𝑆) → ∅ ∈ 𝑆)
2928adantr 468 . . . . . 6 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ∅ ∈ 𝑆)
30 ovex 6916 . . . . . 6 ((𝑀‘∅) /𝑒 𝐴) ∈ V
3129, 30jctir 512 . . . . 5 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (∅ ∈ 𝑆 ∧ ((𝑀‘∅) /𝑒 𝐴) ∈ V))
32 fveq2 6418 . . . . . . 7 (𝑥 = ∅ → (𝑀𝑥) = (𝑀‘∅))
3332oveq1d 6899 . . . . . 6 (𝑥 = ∅ → ((𝑀𝑥) /𝑒 𝐴) = ((𝑀‘∅) /𝑒 𝐴))
3433, 10fvmptg 6511 . . . . 5 ((∅ ∈ 𝑆 ∧ ((𝑀‘∅) /𝑒 𝐴) ∈ V) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = ((𝑀‘∅) /𝑒 𝐴))
3531, 34syl 17 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = ((𝑀‘∅) /𝑒 𝐴))
36 measvnul 30617 . . . . . 6 (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
3736oveq1d 6899 . . . . 5 (𝑀 ∈ (measures‘𝑆) → ((𝑀‘∅) /𝑒 𝐴) = (0 /𝑒 𝐴))
38 xdiv0rp 29986 . . . . 5 (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0)
3937, 38sylan9eq 2871 . . . 4 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑀‘∅) /𝑒 𝐴) = 0)
4035, 39eqtrd 2851 . . 3 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = 0)
41 simpll 774 . . . . . 6 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+))
42 simplr 776 . . . . . . 7 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑦 ∈ 𝒫 𝑆)
43 simprl 778 . . . . . . 7 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑦 ≼ ω)
44 simprr 780 . . . . . . 7 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → Disj 𝑧𝑦 𝑧)
4542, 43, 443jca 1151 . . . . . 6 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧))
469a1i 11 . . . . . . . . 9 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → 𝑦 ∈ V)
47 simplll 782 . . . . . . . . . 10 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧𝑦) → 𝑀 ∈ (measures‘𝑆))
48 simplr 776 . . . . . . . . . . 11 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧𝑦) → 𝑦 ∈ 𝒫 𝑆)
49 simpr 473 . . . . . . . . . . 11 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧𝑦) → 𝑧𝑦)
50 elpwg 4370 . . . . . . . . . . . . 13 (𝑦 ∈ V → (𝑦 ∈ 𝒫 𝑆𝑦𝑆))
519, 50ax-mp 5 . . . . . . . . . . . 12 (𝑦 ∈ 𝒫 𝑆𝑦𝑆)
52 ssel2 3804 . . . . . . . . . . . 12 ((𝑦𝑆𝑧𝑦) → 𝑧𝑆)
5351, 52sylanb 572 . . . . . . . . . . 11 ((𝑦 ∈ 𝒫 𝑆𝑧𝑦) → 𝑧𝑆)
5448, 49, 53syl2anc 575 . . . . . . . . . 10 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧𝑦) → 𝑧𝑆)
55 measvxrge0 30616 . . . . . . . . . 10 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑧𝑆) → (𝑀𝑧) ∈ (0[,]+∞))
5647, 54, 55syl2anc 575 . . . . . . . . 9 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ 𝑧𝑦) → (𝑀𝑧) ∈ (0[,]+∞))
57 simplr 776 . . . . . . . . 9 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → 𝐴 ∈ ℝ+)
5846, 56, 57esumdivc 30493 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → (Σ*𝑧𝑦(𝑀𝑧) /𝑒 𝐴) = Σ*𝑧𝑦((𝑀𝑧) /𝑒 𝐴))
59583ad2antr1 1232 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (Σ*𝑧𝑦(𝑀𝑧) /𝑒 𝐴) = Σ*𝑧𝑦((𝑀𝑧) /𝑒 𝐴))
6026ad2antrr 708 . . . . . . . . . 10 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑆 ran sigAlgebra)
61 simpr1 1241 . . . . . . . . . 10 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑦 ∈ 𝒫 𝑆)
62 simpr2 1243 . . . . . . . . . 10 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑦 ≼ ω)
63 sigaclcu 30528 . . . . . . . . . 10 ((𝑆 ran sigAlgebra ∧ 𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω) → 𝑦𝑆)
6460, 61, 62, 63syl3anc 1483 . . . . . . . . 9 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑦𝑆)
65 fveq2 6418 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀 𝑦))
6665oveq1d 6899 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝑀𝑥) /𝑒 𝐴) = ((𝑀 𝑦) /𝑒 𝐴))
6766, 10, 2fvmpt3i 6518 . . . . . . . . 9 ( 𝑦𝑆 → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = ((𝑀 𝑦) /𝑒 𝐴))
6864, 67syl 17 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = ((𝑀 𝑦) /𝑒 𝐴))
69 simpll 774 . . . . . . . . . . 11 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → 𝑀 ∈ (measures‘𝑆))
7069, 61jca 503 . . . . . . . . . 10 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (𝑀 ∈ (measures‘𝑆) ∧ 𝑦 ∈ 𝒫 𝑆))
71 simpr3 1245 . . . . . . . . . . 11 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → Disj 𝑧𝑦 𝑧)
7262, 71jca 503 . . . . . . . . . 10 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧))
73 measvun 30620 . . . . . . . . . . . . 13 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑦 ∈ 𝒫 𝑆 ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (𝑀 𝑦) = Σ*𝑧𝑦(𝑀𝑧))
74733expia 1143 . . . . . . . . . . . 12 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑦 ∈ 𝒫 𝑆) → ((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → (𝑀 𝑦) = Σ*𝑧𝑦(𝑀𝑧)))
7574ralrimiva 3165 . . . . . . . . . . 11 (𝑀 ∈ (measures‘𝑆) → ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → (𝑀 𝑦) = Σ*𝑧𝑦(𝑀𝑧)))
7675r19.21bi 3131 . . . . . . . . . 10 ((𝑀 ∈ (measures‘𝑆) ∧ 𝑦 ∈ 𝒫 𝑆) → ((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → (𝑀 𝑦) = Σ*𝑧𝑦(𝑀𝑧)))
7770, 72, 76sylc 65 . . . . . . . . 9 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → (𝑀 𝑦) = Σ*𝑧𝑦(𝑀𝑧))
7877oveq1d 6899 . . . . . . . 8 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → ((𝑀 𝑦) /𝑒 𝐴) = (Σ*𝑧𝑦(𝑀𝑧) /𝑒 𝐴))
7968, 78eqtrd 2851 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = (Σ*𝑧𝑦(𝑀𝑧) /𝑒 𝐴))
80 fveq2 6418 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑀𝑥) = (𝑀𝑧))
8180oveq1d 6899 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((𝑀𝑥) /𝑒 𝐴) = ((𝑀𝑧) /𝑒 𝐴))
8281, 10, 2fvmpt3i 6518 . . . . . . . . . 10 (𝑧𝑆 → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧) = ((𝑀𝑧) /𝑒 𝐴))
8353, 82syl 17 . . . . . . . . 9 ((𝑦 ∈ 𝒫 𝑆𝑧𝑦) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧) = ((𝑀𝑧) /𝑒 𝐴))
8483esumeq2dv 30448 . . . . . . . 8 (𝑦 ∈ 𝒫 𝑆 → Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧) = Σ*𝑧𝑦((𝑀𝑧) /𝑒 𝐴))
8561, 84syl 17 . . . . . . 7 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧) = Σ*𝑧𝑦((𝑀𝑧) /𝑒 𝐴))
8659, 79, 853eqtr4d 2861 . . . . . 6 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ (𝑦 ∈ 𝒫 𝑆𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧))
8741, 45, 86syl2anc 575 . . . . 5 ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) ∧ (𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧)) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧))
8887ex 399 . . . 4 (((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) ∧ 𝑦 ∈ 𝒫 𝑆) → ((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧)))
8988ralrimiva 3165 . . 3 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧)))
9025, 40, 893jca 1151 . 2 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧))))
91 ismeas 30610 . . . . 5 (𝑆 ran sigAlgebra → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆) ↔ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧)))))
9226, 91syl 17 . . . 4 (𝑀 ∈ (measures‘𝑆) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆) ↔ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧)))))
9392biimprd 239 . . 3 (𝑀 ∈ (measures‘𝑆) → (((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧))) → (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆)))
9493adantr 468 . 2 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)):𝑆⟶(0[,]+∞) ∧ ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘∅) = 0 ∧ ∀𝑦 ∈ 𝒫 𝑆((𝑦 ≼ ω ∧ Disj 𝑧𝑦 𝑧) → ((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘ 𝑦) = Σ*𝑧𝑦((𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴))‘𝑧))) → (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆)))
9590, 94mpd 15 1 ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥𝑆 ↦ ((𝑀𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wral 3107  wrex 3108  Vcvv 3402  wss 3780  c0 4127  𝒫 cpw 4362   cuni 4641  Disj wdisj 4823   class class class wbr 4855  cmpt 4934  dom cdm 5324  ran crn 5325  Fun wfun 6105   Fn wfn 6106  wf 6107  cfv 6111  (class class class)co 6884  ωcom 7305  cdom 8200  0cc0 10231  +∞cpnf 10366  +crp 12066  [,]cicc 12416   /𝑒 cxdiv 29973  Σ*cesum 30437  sigAlgebracsiga 30518  measurescmeas 30606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-disj 4824  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-of 7137  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-oadd 7810  df-er 7989  df-map 8104  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-fi 8566  df-sup 8597  df-inf 8598  df-oi 8664  df-card 9058  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-q 12028  df-rp 12067  df-xneg 12182  df-xadd 12183  df-xmul 12184  df-ioo 12417  df-ioc 12418  df-ico 12419  df-icc 12420  df-fz 12570  df-fzo 12710  df-seq 13045  df-hash 13358  df-struct 16090  df-ndx 16091  df-slot 16092  df-base 16094  df-sets 16095  df-ress 16096  df-plusg 16186  df-mulr 16187  df-tset 16192  df-ple 16193  df-ds 16195  df-rest 16308  df-topn 16309  df-0g 16327  df-gsum 16328  df-topgen 16329  df-ordt 16386  df-xrs 16387  df-mre 16471  df-mrc 16472  df-acs 16474  df-ps 17425  df-tsr 17426  df-mgm 17467  df-sgrp 17509  df-mnd 17520  df-mhm 17560  df-submnd 17561  df-cntz 17971  df-cmn 18416  df-fbas 19971  df-fg 19972  df-top 20933  df-topon 20950  df-topsp 20972  df-bases 20985  df-ntr 21059  df-nei 21137  df-cn 21266  df-cnp 21267  df-haus 21354  df-fil 21884  df-fm 21976  df-flim 21977  df-flf 21978  df-tsms 22164  df-xdiv 29974  df-esum 30438  df-siga 30519  df-meas 30607
This theorem is referenced by:  probfinmeasbOLD  30838  probmeasb  30840
  Copyright terms: Public domain W3C validator