Metamath Proof Explorer

Theorem measinb

Description: Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measinb 
|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) e. ( measures ` S ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x e. S ) -> M e. ( measures ` S ) )
2 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
3 2 ad2antrr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x e. S ) -> S e. U. ran sigAlgebra )
4 simpr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x e. S ) -> x e. S )
5 simplr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x e. S ) -> A e. S )
6 inelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ x e. S /\ A e. S ) -> ( x i^i A ) e. S )
7 3 4 5 6 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x e. S ) -> ( x i^i A ) e. S )
8 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( x i^i A ) e. S ) -> ( M ` ( x i^i A ) ) e. ( 0 [,] +oo ) )
9 1 7 8 syl2anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x e. S ) -> ( M ` ( x i^i A ) ) e. ( 0 [,] +oo ) )
10 9 fmpttd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) : S --> ( 0 [,] +oo ) )
11 eqidd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) = ( x e. S |-> ( M ` ( x i^i A ) ) ) )
12 ineq1 
 |-  ( x = (/) -> ( x i^i A ) = ( (/) i^i A ) )
13 0in 
 |-  ( (/) i^i A ) = (/)
14 12 13 eqtrdi 
 |-  ( x = (/) -> ( x i^i A ) = (/) )
15 14 fveq2d 
 |-  ( x = (/) -> ( M ` ( x i^i A ) ) = ( M ` (/) ) )
16 15 adantl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x = (/) ) -> ( M ` ( x i^i A ) ) = ( M ` (/) ) )
17 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
18 17 ad2antrr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x = (/) ) -> ( M ` (/) ) = 0 )
19 16 18 eqtrd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ x = (/) ) -> ( M ` ( x i^i A ) ) = 0 )
20 2 adantr 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> S e. U. ran sigAlgebra )
21 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
22 20 21 syl 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> (/) e. S )
23 0red 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> 0 e. RR )
24 11 19 22 23 fvmptd 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` (/) ) = 0 )
25 measinblem 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> ( M ` ( U. z i^i A ) ) = sum* y e. z ( M ` ( y i^i A ) ) )
26 eqidd 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) = ( x e. S |-> ( M ` ( x i^i A ) ) ) )
27 ineq1 
 |-  ( x = U. z -> ( x i^i A ) = ( U. z i^i A ) )
28 27 adantl 
 |-  ( ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) /\ x = U. z ) -> ( x i^i A ) = ( U. z i^i A ) )
29 28 fveq2d 
 |-  ( ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) /\ x = U. z ) -> ( M ` ( x i^i A ) ) = ( M ` ( U. z i^i A ) ) )
30 simplll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> M e. ( measures ` S ) )
31 30 2 syl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> S e. U. ran sigAlgebra )
32 simplr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> z e. ~P S )
33 simprl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> z ~<_ _om )
34 sigaclcu 
 |-  ( ( S e. U. ran sigAlgebra /\ z e. ~P S /\ z ~<_ _om ) -> U. z e. S )
35 31 32 33 34 syl3anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> U. z e. S )
36 simpllr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> A e. S )
37 inelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ U. z e. S /\ A e. S ) -> ( U. z i^i A ) e. S )
38 31 35 36 37 syl3anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> ( U. z i^i A ) e. S )
39 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( U. z i^i A ) e. S ) -> ( M ` ( U. z i^i A ) ) e. ( 0 [,] +oo ) )
40 30 38 39 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> ( M ` ( U. z i^i A ) ) e. ( 0 [,] +oo ) )
41 26 29 35 40 fvmptd 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` U. z ) = ( M ` ( U. z i^i A ) ) )
42 eqidd 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) = ( x e. S |-> ( M ` ( x i^i A ) ) ) )
43 ineq1 
 |-  ( x = y -> ( x i^i A ) = ( y i^i A ) )
44 43 adantl 
 |-  ( ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) /\ x = y ) -> ( x i^i A ) = ( y i^i A ) )
45 44 fveq2d 
 |-  ( ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) /\ x = y ) -> ( M ` ( x i^i A ) ) = ( M ` ( y i^i A ) ) )
46 elpwi 
 |-  ( z e. ~P S -> z C_ S )
47 46 ad2antlr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> z C_ S )
48 simpr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> y e. z )
49 47 48 sseldd 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> y e. S )
50 simplll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> M e. ( measures ` S ) )
51 50 2 syl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> S e. U. ran sigAlgebra )
52 simpllr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> A e. S )
53 inelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ y e. S /\ A e. S ) -> ( y i^i A ) e. S )
54 51 49 52 53 syl3anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> ( y i^i A ) e. S )
55 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ ( y i^i A ) e. S ) -> ( M ` ( y i^i A ) ) e. ( 0 [,] +oo ) )
56 50 54 55 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> ( M ` ( y i^i A ) ) e. ( 0 [,] +oo ) )
57 42 45 49 56 fvmptd 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ y e. z ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) = ( M ` ( y i^i A ) ) )
58 57 esumeq2dv 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) -> sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) = sum* y e. z ( M ` ( y i^i A ) ) )
59 58 adantr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) = sum* y e. z ( M ` ( y i^i A ) ) )
60 25 41 59 3eqtr4d 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) /\ ( z ~<_ _om /\ Disj_ y e. z y ) ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` U. z ) = sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) )
61 60 ex 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ z e. ~P S ) -> ( ( z ~<_ _om /\ Disj_ y e. z y ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` U. z ) = sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) ) )
62 61 ralrimiva 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` U. z ) = sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) ) )
63 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) e. ( measures ` S ) <-> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` (/) ) = 0 /\ A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` U. z ) = sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) ) ) ) )
64 20 63 syl 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) e. ( measures ` S ) <-> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` (/) ) = 0 /\ A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` U. z ) = sum* y e. z ( ( x e. S |-> ( M ` ( x i^i A ) ) ) ` y ) ) ) ) )
65 10 24 62 64 mpbir3and 
 |-  ( ( M e. ( measures ` S ) /\ A e. S ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) e. ( measures ` S ) )