Metamath Proof Explorer

Theorem measdivcst

Description: Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016) (Revised by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Assertion measdivcst ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) ∈ ( measures ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ofcfval3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) = ( 𝑥 ∈ dom 𝑀 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) )
2 measfrge0 ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
3 2 fdmd ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → dom 𝑀 = 𝑆 )
4 3 adantr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → dom 𝑀 = 𝑆 )
5 4 mpteq1d ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑥 ∈ dom 𝑀 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) )
6 1 5 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) )
7 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
8 7 adantlr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
9 simplr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ+ )
10 8 9 xrpxdivcld ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ∈ ( 0 [,] +∞ ) )
11 10 fmpttd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
12 measbase ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
13 0elsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )
14 12 13 syl ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ∅ ∈ 𝑆 )
15 14 adantr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ∅ ∈ 𝑆 )
16 ovex ⊢ ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ∈ V
17 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∅ ) )
18 17 oveq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) = ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) )
19 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) )
20 18 19 fvmptg ⊢ ( ( ∅ ∈ 𝑆 ∧ ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) ∈ V ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) )
21 15 16 20 sylancl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) )
22 measvnul ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )
23 22 oveq1d ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) = ( 0 /𝑒 𝐴 ) )
24 xdiv0rp ⊢ ( 𝐴 ∈ ℝ+ → ( 0 /𝑒 𝐴 ) = 0 )
25 23 24 sylan9eq ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑀 ‘ ∅ ) /𝑒 𝐴 ) = 0 )
26 21 25 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 )
27 simpll ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) )
28 simplr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ∈ 𝒫 𝑆 )
29 simprl ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ≼ ω )
30 simprr ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → Disj 𝑧 ∈ 𝑦 𝑧 )
31 vex ⊢ 𝑦 ∈ V
32 31 a1i ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → 𝑦 ∈ V )
33 simplll ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
34 velpw ⊢ ( 𝑦 ∈ 𝒫 𝑆 ↔ 𝑦 ⊆ 𝑆 )
35 ssel2 ⊢ ( ( 𝑦 ⊆ 𝑆 ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑆 )
36 34 35 sylanb ⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑆 )
37 36 adantll ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑆 )
38 measvxrge0 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
39 33 37 38 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑧 ∈ 𝑦 ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
40 simplr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → 𝐴 ∈ ℝ+ )
41 32 39 40 esumdivc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
42 41 3ad2antr1 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
43 12 ad2antrr ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
44 simpr1 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ∈ 𝒫 𝑆 )
45 simpr2 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑦 ≼ ω )
46 sigaclcu ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ 𝑆 )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ∪ 𝑦 ∈ 𝑆 )
48 fveq2 ⊢ ( 𝑥 = ∪ 𝑦 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑦 ) )
49 48 oveq1d ⊢ ( 𝑥 = ∪ 𝑦 → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) = ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) )
50 ovex ⊢ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ∈ V
51 49 19 50 fvmpt3i ⊢ ( ∪ 𝑦 ∈ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) )
52 47 51 syl ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) )
53 simpll ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
54 simpr3 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → Disj 𝑧 ∈ 𝑦 𝑧 )
55 measvun ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑦 ∈ 𝒫 𝑆 ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) )
56 53 44 45 54 55 syl112anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( 𝑀 ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) )
57 56 oveq1d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑀 ‘ ∪ 𝑦 ) /𝑒 𝐴 ) = ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
58 52 57 eqtrd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = ( Σ* 𝑧 ∈ 𝑦 ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
59 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑧 ) )
60 59 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) = ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
61 60 19 50 fvmpt3i ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
62 36 61 syl ⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑧 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
63 62 esumeq2dv ⊢ ( 𝑦 ∈ 𝒫 𝑆 → Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
64 44 63 syl ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑀 ‘ 𝑧 ) /𝑒 𝐴 ) )
65 42 58 64 3eqtr4d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) )
66 27 28 29 30 65 syl13anc ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) )
67 66 ex ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝒫 𝑆 ) → ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) )
68 67 ralrimiva ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) )
69 ismeas ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) ) )
70 12 69 syl ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) ) )
71 70 biimprd ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ) )
72 71 adantr ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∅ ) = 0 ∧ ∀ 𝑦 ∈ 𝒫 𝑆 ( ( 𝑦 ≼ ω ∧ Disj 𝑧 ∈ 𝑦 𝑧 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ ∪ 𝑦 ) = Σ* 𝑧 ∈ 𝑦 ( ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ‘ 𝑧 ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) ) )
73 11 26 68 72 mp3and ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑀 ‘ 𝑥 ) /𝑒 𝐴 ) ) ∈ ( measures ‘ 𝑆 ) )
74 6 73 eqeltrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 ∘f/c /𝑒 𝐴 ) ∈ ( measures ‘ 𝑆 ) )