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 
|- ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( M oFC /e A ) e. ( measures ` S ) )

Proof

Step Hyp Ref Expression
1 ofcfval3 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( M oFC /e A ) = ( x e. dom M |-> ( ( M ` x ) /e A ) ) )
2 measfrge0 
 |-  ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )
3 2 fdmd 
 |-  ( M e. ( measures ` S ) -> dom M = S )
4 3 adantr 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> dom M = S )
5 4 mpteq1d 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. dom M |-> ( ( M ` x ) /e A ) ) = ( x e. S |-> ( ( M ` x ) /e A ) ) )
6 1 5 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( M oFC /e A ) = ( x e. S |-> ( ( M ` x ) /e A ) ) )
7 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
8 7 adantlr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
9 simplr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> A e. RR+ )
10 8 9 xrpxdivcld 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( ( M ` x ) /e A ) e. ( 0 [,] +oo ) )
11 10 fmpttd 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) )
12 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
13 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
14 12 13 syl 
 |-  ( M e. ( measures ` S ) -> (/) e. S )
15 14 adantr 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> (/) e. S )
16 ovex 
 |-  ( ( M ` (/) ) /e A ) e. _V
17 fveq2 
 |-  ( x = (/) -> ( M ` x ) = ( M ` (/) ) )
18 17 oveq1d 
 |-  ( x = (/) -> ( ( M ` x ) /e A ) = ( ( M ` (/) ) /e A ) )
19 eqid 
 |-  ( x e. S |-> ( ( M ` x ) /e A ) ) = ( x e. S |-> ( ( M ` x ) /e A ) )
20 18 19 fvmptg 
 |-  ( ( (/) e. S /\ ( ( M ` (/) ) /e A ) e. _V ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = ( ( M ` (/) ) /e A ) )
21 15 16 20 sylancl 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = ( ( M ` (/) ) /e A ) )
22 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
23 22 oveq1d 
 |-  ( M e. ( measures ` S ) -> ( ( M ` (/) ) /e A ) = ( 0 /e A ) )
24 xdiv0rp 
 |-  ( A e. RR+ -> ( 0 /e A ) = 0 )
25 23 24 sylan9eq 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( M ` (/) ) /e A ) = 0 )
26 21 25 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 )
27 simpll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M e. ( measures ` S ) /\ A e. RR+ ) )
28 simplr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> y e. ~P S )
29 simprl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> y ~<_ _om )
30 simprr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> Disj_ z e. y z )
31 vex 
 |-  y e. _V
32 31 a1i 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> y e. _V )
33 simplll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> M e. ( measures ` S ) )
34 velpw 
 |-  ( y e. ~P S <-> y C_ S )
35 ssel2 
 |-  ( ( y C_ S /\ z e. y ) -> z e. S )
36 34 35 sylanb 
 |-  ( ( y e. ~P S /\ z e. y ) -> z e. S )
37 36 adantll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> z e. S )
38 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ z e. S ) -> ( M ` z ) e. ( 0 [,] +oo ) )
39 33 37 38 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> ( M ` z ) e. ( 0 [,] +oo ) )
40 simplr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> A e. RR+ )
41 32 39 40 esumdivc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> ( sum* z e. y ( M ` z ) /e A ) = sum* z e. y ( ( M ` z ) /e A ) )
42 41 3ad2antr1 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( sum* z e. y ( M ` z ) /e A ) = sum* z e. y ( ( M ` z ) /e A ) )
43 12 ad2antrr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> S e. U. ran sigAlgebra )
44 simpr1 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> y e. ~P S )
45 simpr2 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> y ~<_ _om )
46 sigaclcu 
 |-  ( ( S e. U. ran sigAlgebra /\ y e. ~P S /\ y ~<_ _om ) -> U. y e. S )
47 43 44 45 46 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> U. y e. S )
48 fveq2 
 |-  ( x = U. y -> ( M ` x ) = ( M ` U. y ) )
49 48 oveq1d 
 |-  ( x = U. y -> ( ( M ` x ) /e A ) = ( ( M ` U. y ) /e A ) )
50 ovex 
 |-  ( ( M ` x ) /e A ) e. _V
51 49 19 50 fvmpt3i 
 |-  ( U. y e. S -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = ( ( M ` U. y ) /e A ) )
52 47 51 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = ( ( M ` U. y ) /e A ) )
53 simpll 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> M e. ( measures ` S ) )
54 simpr3 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> Disj_ z e. y z )
55 measvun 
 |-  ( ( M e. ( measures ` S ) /\ y e. ~P S /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) )
56 53 44 45 54 55 syl112anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) )
57 56 oveq1d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( M ` U. y ) /e A ) = ( sum* z e. y ( M ` z ) /e A ) )
58 52 57 eqtrd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = ( sum* z e. y ( M ` z ) /e A ) )
59 fveq2 
 |-  ( x = z -> ( M ` x ) = ( M ` z ) )
60 59 oveq1d 
 |-  ( x = z -> ( ( M ` x ) /e A ) = ( ( M ` z ) /e A ) )
61 60 19 50 fvmpt3i 
 |-  ( z e. S -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = ( ( M ` z ) /e A ) )
62 36 61 syl 
 |-  ( ( y e. ~P S /\ z e. y ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = ( ( M ` z ) /e A ) )
63 62 esumeq2dv 
 |-  ( y e. ~P S -> sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = sum* z e. y ( ( M ` z ) /e A ) )
64 44 63 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = sum* z e. y ( ( M ` z ) /e A ) )
65 42 58 64 3eqtr4d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) )
66 27 28 29 30 65 syl13anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) )
67 66 ex 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) )
68 67 ralrimiva 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) )
69 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) <-> ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) ) )
70 12 69 syl 
 |-  ( M e. ( measures ` S ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) <-> ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) ) )
71 70 biimprd 
 |-  ( M e. ( measures ` S ) -> ( ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) ) )
72 71 adantr 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) ) )
73 11 26 68 72 mp3and 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) )
74 6 73 eqeltrd 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( M oFC /e A ) e. ( measures ` S ) )