Metamath Proof Explorer

Theorem measinblem

Description: Lemma for measinb . (Contributed by Thierry Arnoux, 2-Jun-2017)

Ref Expression
Assertion measinblem 
|- ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> ( M ` ( U. B i^i A ) ) = sum* x e. B ( M ` ( x i^i A ) ) )

Proof

Step Hyp Ref Expression
1 iunin1 
 |-  U_ x e. B ( x i^i A ) = ( U_ x e. B x i^i A )
2 uniiun 
 |-  U. B = U_ x e. B x
3 2 ineq1i 
 |-  ( U. B i^i A ) = ( U_ x e. B x i^i A )
4 1 3 eqtr4i 
 |-  U_ x e. B ( x i^i A ) = ( U. B i^i A )
5 4 fveq2i 
 |-  ( M ` U_ x e. B ( x i^i A ) ) = ( M ` ( U. B i^i A ) )
6 simplll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> M e. ( measures ` S ) )
7 nfv 
 |-  F/ x ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S )
8 nfv 
 |-  F/ x B ~<_ _om
9 nfdisj1 
 |-  F/ x Disj_ x e. B x
10 8 9 nfan 
 |-  F/ x ( B ~<_ _om /\ Disj_ x e. B x )
11 7 10 nfan 
 |-  F/ x ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) )
12 simp1ll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> M e. ( measures ` S ) )
13 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
14 12 13 syl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> S e. U. ran sigAlgebra )
15 simp3 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> x e. B )
16 simp1r 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> B e. ~P S )
17 elelpwi 
 |-  ( ( x e. B /\ B e. ~P S ) -> x e. S )
18 15 16 17 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> x e. S )
19 simp1lr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> A e. S )
20 inelsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ x e. S /\ A e. S ) -> ( x i^i A ) e. S )
21 14 18 19 20 syl3anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) /\ x e. B ) -> ( x i^i A ) e. S )
22 21 3expia 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> ( x e. B -> ( x i^i A ) e. S ) )
23 11 22 ralrimi 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> A. x e. B ( x i^i A ) e. S )
24 simprl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> B ~<_ _om )
25 disjin 
 |-  ( Disj_ x e. B x -> Disj_ x e. B ( x i^i A ) )
26 25 ad2antll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> Disj_ x e. B ( x i^i A ) )
27 measvuni 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. B ( x i^i A ) e. S /\ ( B ~<_ _om /\ Disj_ x e. B ( x i^i A ) ) ) -> ( M ` U_ x e. B ( x i^i A ) ) = sum* x e. B ( M ` ( x i^i A ) ) )
28 6 23 24 26 27 syl112anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> ( M ` U_ x e. B ( x i^i A ) ) = sum* x e. B ( M ` ( x i^i A ) ) )
29 5 28 eqtr3id 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. S ) /\ B e. ~P S ) /\ ( B ~<_ _om /\ Disj_ x e. B x ) ) -> ( M ` ( U. B i^i A ) ) = sum* x e. B ( M ` ( x i^i A ) ) )