Metamath Proof Explorer

Theorem measres

Description: Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measres 
|- ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( M |` T ) e. ( measures ` T ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> T e. U. ran sigAlgebra )
2 measfrge0 
 |-  ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )
3 2 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> M : S --> ( 0 [,] +oo ) )
4 simp3 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> T C_ S )
5 3 4 fssresd 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( M |` T ) : T --> ( 0 [,] +oo ) )
6 0elsiga 
 |-  ( T e. U. ran sigAlgebra -> (/) e. T )
7 fvres 
 |-  ( (/) e. T -> ( ( M |` T ) ` (/) ) = ( M ` (/) ) )
8 1 6 7 3syl 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( ( M |` T ) ` (/) ) = ( M ` (/) ) )
9 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
10 9 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( M ` (/) ) = 0 )
11 8 10 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( ( M |` T ) ` (/) ) = 0 )
12 simp11 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> M e. ( measures ` S ) )
13 simp13 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> T C_ S )
14 simp2 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> x e. ~P T )
15 sspw 
 |-  ( T C_ S -> ~P T C_ ~P S )
16 15 sselda 
 |-  ( ( T C_ S /\ x e. ~P T ) -> x e. ~P S )
17 13 14 16 syl2anc 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> x e. ~P S )
18 simp3 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( x ~<_ _om /\ Disj_ y e. x y ) )
19 measvun 
 |-  ( ( M e. ( measures ` S ) /\ x e. ~P S /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) )
20 12 17 18 19 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) )
21 1 3ad2ant1 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> T e. U. ran sigAlgebra )
22 simp3l 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> x ~<_ _om )
23 sigaclcu 
 |-  ( ( T e. U. ran sigAlgebra /\ x e. ~P T /\ x ~<_ _om ) -> U. x e. T )
24 21 14 22 23 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> U. x e. T )
25 24 fvresd 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( ( M |` T ) ` U. x ) = ( M ` U. x ) )
26 elpwi 
 |-  ( x e. ~P T -> x C_ T )
27 26 sselda 
 |-  ( ( x e. ~P T /\ y e. x ) -> y e. T )
28 27 adantll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T ) /\ y e. x ) -> y e. T )
29 28 fvresd 
 |-  ( ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T ) /\ y e. x ) -> ( ( M |` T ) ` y ) = ( M ` y ) )
30 29 esumeq2dv 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T ) -> sum* y e. x ( ( M |` T ) ` y ) = sum* y e. x ( M ` y ) )
31 30 3adant3 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> sum* y e. x ( ( M |` T ) ` y ) = sum* y e. x ( M ` y ) )
32 20 25 31 3eqtr4d 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( ( M |` T ) ` U. x ) = sum* y e. x ( ( M |` T ) ` y ) )
33 32 3expia 
 |-  ( ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) /\ x e. ~P T ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( M |` T ) ` U. x ) = sum* y e. x ( ( M |` T ) ` y ) ) )
34 33 ralrimiva 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> A. x e. ~P T ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( M |` T ) ` U. x ) = sum* y e. x ( ( M |` T ) ` y ) ) )
35 5 11 34 3jca 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( ( M |` T ) : T --> ( 0 [,] +oo ) /\ ( ( M |` T ) ` (/) ) = 0 /\ A. x e. ~P T ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( M |` T ) ` U. x ) = sum* y e. x ( ( M |` T ) ` y ) ) ) )
36 ismeas 
 |-  ( T e. U. ran sigAlgebra -> ( ( M |` T ) e. ( measures ` T ) <-> ( ( M |` T ) : T --> ( 0 [,] +oo ) /\ ( ( M |` T ) ` (/) ) = 0 /\ A. x e. ~P T ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( M |` T ) ` U. x ) = sum* y e. x ( ( M |` T ) ` y ) ) ) ) )
37 36 biimprd 
 |-  ( T e. U. ran sigAlgebra -> ( ( ( M |` T ) : T --> ( 0 [,] +oo ) /\ ( ( M |` T ) ` (/) ) = 0 /\ A. x e. ~P T ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( M |` T ) ` U. x ) = sum* y e. x ( ( M |` T ) ` y ) ) ) -> ( M |` T ) e. ( measures ` T ) ) )
38 1 35 37 sylc 
 |-  ( ( M e. ( measures ` S ) /\ T e. U. ran sigAlgebra /\ T C_ S ) -> ( M |` T ) e. ( measures ` T ) )