Theorem measinb2

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

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

Proof

Step	Hyp	Ref	Expression
1		resmpt3	|- ( ( x e. S |-> ( M ` ( x i^i A ) ) ) |` ( S i^i ~P A ) ) = ( x e. ( S i^i ( S i^i ~P A ) ) |-> ( M ` ( x i^i A ) ) )
2		inin	|- ( S i^i ( S i^i ~P A ) ) = ( S i^i ~P A )
3		eqid	|- ( M ` ( x i^i A ) ) = ( M ` ( x i^i A ) )
4	2 3	mpteq12i	|- ( x e. ( S i^i ( S i^i ~P A ) ) |-> ( M ` ( x i^i A ) ) ) = ( x e. ( S i^i ~P A ) |-> ( M ` ( x i^i A ) ) )
5	1 4	eqtri	|- ( ( x e. S |-> ( M ` ( x i^i A ) ) ) |` ( S i^i ~P A ) ) = ( x e. ( S i^i ~P A ) |-> ( M ` ( x i^i A ) ) )
6		measinb	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( x e. S |-> ( M ` ( x i^i A ) ) ) e. ( measures ` S ) )
7		measbase	|- ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
8		sigainb	|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. ( sigAlgebra ` A ) )
9		elrnsiga	|- ( ( S i^i ~P A ) e. ( sigAlgebra ` A ) -> ( S i^i ~P A ) e. U. ran sigAlgebra )
10	8 9	syl	|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. U. ran sigAlgebra )
11	7 10	sylan	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( S i^i ~P A ) e. U. ran sigAlgebra )
12		inss1	|- ( S i^i ~P A ) C_ S
13	12	a1i	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( S i^i ~P A ) C_ S )
14		measres	|- ( ( ( x e. S |-> ( M ` ( x i^i A ) ) ) e. ( measures ` S ) /\ ( S i^i ~P A ) e. U. ran sigAlgebra /\ ( S i^i ~P A ) C_ S ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) |` ( S i^i ~P A ) ) e. ( measures ` ( S i^i ~P A ) ) )
15	6 11 13 14	syl3anc	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( ( x e. S |-> ( M ` ( x i^i A ) ) ) |` ( S i^i ~P A ) ) e. ( measures ` ( S i^i ~P A ) ) )
16	5 15	eqeltrrid	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( x e. ( S i^i ~P A ) |-> ( M ` ( x i^i A ) ) ) e. ( measures ` ( S i^i ~P A ) ) )