Metamath Proof Explorer

Theorem measvunilem0

Description: Lemma for measvuni . (Contributed by Thierry Arnoux, 6-Mar-2017)

Ref Expression
Hypothesis measvunilem.0.1 
|- F/_ x A
Assertion measvunilem0 
|- ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = sum* x e. A ( M ` B ) )

Proof

Step Hyp Ref Expression
1 measvunilem.0.1 
 |-  F/_ x A
2 simp3l 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A ~<_ _om )
3 ctex 
 |-  ( A ~<_ _om -> A e. _V )
4 1 esum0 
 |-  ( A e. _V -> sum* x e. A 0 = 0 )
5 2 3 4 3syl 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> sum* x e. A 0 = 0 )
6 nfv 
 |-  F/ x M e. ( measures ` S )
7 nfra1 
 |-  F/ x A. x e. A B e. { (/) }
8 nfcv 
 |-  F/_ x ~<_
9 nfcv 
 |-  F/_ x _om
10 1 8 9 nfbr 
 |-  F/ x A ~<_ _om
11 nfdisj1 
 |-  F/ x Disj_ x e. A B
12 10 11 nfan 
 |-  F/ x ( A ~<_ _om /\ Disj_ x e. A B )
13 6 7 12 nf3an 
 |-  F/ x ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) )
14 eqidd 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A = A )
15 simp2 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> A. x e. A B e. { (/) } )
16 15 r19.21bi 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> B e. { (/) } )
17 elsni 
 |-  ( B e. { (/) } -> B = (/) )
18 16 17 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> B = (/) )
19 18 fveq2d 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> ( M ` B ) = ( M ` (/) ) )
20 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
21 20 3ad2ant1 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` (/) ) = 0 )
22 21 adantr 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> ( M ` (/) ) = 0 )
23 19 22 eqtrd 
 |-  ( ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) /\ x e. A ) -> ( M ` B ) = 0 )
24 13 14 23 esumeq12dvaf 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> sum* x e. A ( M ` B ) = sum* x e. A 0 )
25 13 1 1 14 18 iuneq12daf 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> U_ x e. A B = U_ x e. A (/) )
26 iun0 
 |-  U_ x e. A (/) = (/)
27 25 26 eqtrdi 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> U_ x e. A B = (/) )
28 27 fveq2d 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = ( M ` (/) ) )
29 28 21 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = 0 )
30 5 24 29 3eqtr4rd 
 |-  ( ( M e. ( measures ` S ) /\ A. x e. A B e. { (/) } /\ ( A ~<_ _om /\ Disj_ x e. A B ) ) -> ( M ` U_ x e. A B ) = sum* x e. A ( M ` B ) )