Metamath Proof Explorer

Theorem meadjiun

Description: The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meadjiun.1 
|- F/ k ph
meadjiun.m 
|- ( ph -> M e. Meas )
meadjiun.s 
|- S = dom M
meadjiun.b 
|- ( ( ph /\ k e. A ) -> B e. S )
meadjiun.a 
|- ( ph -> A ~<_ _om )
meadjiun.dj 
|- ( ph -> Disj_ k e. A B )
Assertion meadjiun 
|- ( ph -> ( M ` U_ k e. A B ) = ( sum^ ` ( k e. A |-> ( M ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 meadjiun.1 
 |-  F/ k ph
2 meadjiun.m 
 |-  ( ph -> M e. Meas )
3 meadjiun.s 
 |-  S = dom M
4 meadjiun.b 
 |-  ( ( ph /\ k e. A ) -> B e. S )
5 meadjiun.a 
 |-  ( ph -> A ~<_ _om )
6 meadjiun.dj 
 |-  ( ph -> Disj_ k e. A B )
7 4 ex 
 |-  ( ph -> ( k e. A -> B e. S ) )
8 1 7 ralrimi 
 |-  ( ph -> A. k e. A B e. S )
9 dfiun3g 
 |-  ( A. k e. A B e. S -> U_ k e. A B = U. ran ( k e. A |-> B ) )
10 8 9 syl 
 |-  ( ph -> U_ k e. A B = U. ran ( k e. A |-> B ) )
11 10 fveq2d 
 |-  ( ph -> ( M ` U_ k e. A B ) = ( M ` U. ran ( k e. A |-> B ) ) )
12 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
13 12 rnmptss 
 |-  ( A. k e. A B e. S -> ran ( k e. A |-> B ) C_ S )
14 8 13 syl 
 |-  ( ph -> ran ( k e. A |-> B ) C_ S )
15 1stcrestlem 
 |-  ( A ~<_ _om -> ran ( k e. A |-> B ) ~<_ _om )
16 5 15 syl 
 |-  ( ph -> ran ( k e. A |-> B ) ~<_ _om )
17 12 disjrnmpt2 
 |-  ( Disj_ k e. A B -> Disj_ x e. ran ( k e. A |-> B ) x )
18 6 17 syl 
 |-  ( ph -> Disj_ x e. ran ( k e. A |-> B ) x )
19 2 3 14 16 18 meadjuni 
 |-  ( ph -> ( M ` U. ran ( k e. A |-> B ) ) = ( sum^ ` ( M |` ran ( k e. A |-> B ) ) ) )
20 reldom 
 |-  Rel ~<_
21 brrelex1 
 |-  ( ( Rel ~<_ /\ A ~<_ _om ) -> A e. _V )
22 20 21 mpan 
 |-  ( A ~<_ _om -> A e. _V )
23 5 22 syl 
 |-  ( ph -> A e. _V )
24 1 4 12 fmptdf 
 |-  ( ph -> ( k e. A |-> B ) : A --> S )
25 fveq2 
 |-  ( j = i -> ( ( k e. A |-> B ) ` j ) = ( ( k e. A |-> B ) ` i ) )
26 25 neeq1d 
 |-  ( j = i -> ( ( ( k e. A |-> B ) ` j ) =/= (/) <-> ( ( k e. A |-> B ) ` i ) =/= (/) ) )
27 26 cbvrabv 
 |-  { j e. A | ( ( k e. A |-> B ) ` j ) =/= (/) } = { i e. A | ( ( k e. A |-> B ) ` i ) =/= (/) }
28 simpr 
 |-  ( ( ph /\ i e. A ) -> i e. A )
29 nfv 
 |-  F/ k i e. A
30 1 29 nfan 
 |-  F/ k ( ph /\ i e. A )
31 nfcv 
 |-  F/_ k i
32 31 nfcsb1 
 |-  F/_ k [_ i / k ]_ B
33 nfcv 
 |-  F/_ k S
34 32 33 nfel 
 |-  F/ k [_ i / k ]_ B e. S
35 30 34 nfim 
 |-  F/ k ( ( ph /\ i e. A ) -> [_ i / k ]_ B e. S )
36 eleq1w 
 |-  ( k = i -> ( k e. A <-> i e. A ) )
37 36 anbi2d 
 |-  ( k = i -> ( ( ph /\ k e. A ) <-> ( ph /\ i e. A ) ) )
38 csbeq1a 
 |-  ( k = i -> B = [_ i / k ]_ B )
39 38 eleq1d 
 |-  ( k = i -> ( B e. S <-> [_ i / k ]_ B e. S ) )
40 37 39 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. A ) -> B e. S ) <-> ( ( ph /\ i e. A ) -> [_ i / k ]_ B e. S ) ) )
41 35 40 4 chvarfv 
 |-  ( ( ph /\ i e. A ) -> [_ i / k ]_ B e. S )
42 31 32 38 12 fvmptf 
 |-  ( ( i e. A /\ [_ i / k ]_ B e. S ) -> ( ( k e. A |-> B ) ` i ) = [_ i / k ]_ B )
43 28 41 42 syl2anc 
 |-  ( ( ph /\ i e. A ) -> ( ( k e. A |-> B ) ` i ) = [_ i / k ]_ B )
44 43 disjeq2dv 
 |-  ( ph -> ( Disj_ i e. A ( ( k e. A |-> B ) ` i ) <-> Disj_ i e. A [_ i / k ]_ B ) )
45 nfcv 
 |-  F/_ i B
46 45 32 38 cbvdisj 
 |-  ( Disj_ k e. A B <-> Disj_ i e. A [_ i / k ]_ B )
47 46 bicomi 
 |-  ( Disj_ i e. A [_ i / k ]_ B <-> Disj_ k e. A B )
48 47 a1i 
 |-  ( ph -> ( Disj_ i e. A [_ i / k ]_ B <-> Disj_ k e. A B ) )
49 44 48 bitrd 
 |-  ( ph -> ( Disj_ i e. A ( ( k e. A |-> B ) ` i ) <-> Disj_ k e. A B ) )
50 6 49 mpbird 
 |-  ( ph -> Disj_ i e. A ( ( k e. A |-> B ) ` i ) )
51 2 3 23 24 27 50 meadjiunlem 
 |-  ( ph -> ( sum^ ` ( M |` ran ( k e. A |-> B ) ) ) = ( sum^ ` ( M o. ( k e. A |-> B ) ) ) )
52 45 32 38 cbvmpt 
 |-  ( k e. A |-> B ) = ( i e. A |-> [_ i / k ]_ B )
53 52 coeq2i 
 |-  ( M o. ( k e. A |-> B ) ) = ( M o. ( i e. A |-> [_ i / k ]_ B ) )
54 53 a1i 
 |-  ( ph -> ( M o. ( k e. A |-> B ) ) = ( M o. ( i e. A |-> [_ i / k ]_ B ) ) )
55 eqidd 
 |-  ( ph -> ( i e. A |-> [_ i / k ]_ B ) = ( i e. A |-> [_ i / k ]_ B ) )
56 2 3 meaf 
 |-  ( ph -> M : S --> ( 0 [,] +oo ) )
57 56 feqmptd 
 |-  ( ph -> M = ( y e. S |-> ( M ` y ) ) )
58 fveq2 
 |-  ( y = [_ i / k ]_ B -> ( M ` y ) = ( M ` [_ i / k ]_ B ) )
59 41 55 57 58 fmptco 
 |-  ( ph -> ( M o. ( i e. A |-> [_ i / k ]_ B ) ) = ( i e. A |-> ( M ` [_ i / k ]_ B ) ) )
60 nfcv 
 |-  F/_ i ( M ` B )
61 nfcv 
 |-  F/_ k M
62 61 32 nffv 
 |-  F/_ k ( M ` [_ i / k ]_ B )
63 38 fveq2d 
 |-  ( k = i -> ( M ` B ) = ( M ` [_ i / k ]_ B ) )
64 60 62 63 cbvmpt 
 |-  ( k e. A |-> ( M ` B ) ) = ( i e. A |-> ( M ` [_ i / k ]_ B ) )
65 64 eqcomi 
 |-  ( i e. A |-> ( M ` [_ i / k ]_ B ) ) = ( k e. A |-> ( M ` B ) )
66 65 a1i 
 |-  ( ph -> ( i e. A |-> ( M ` [_ i / k ]_ B ) ) = ( k e. A |-> ( M ` B ) ) )
67 54 59 66 3eqtrd 
 |-  ( ph -> ( M o. ( k e. A |-> B ) ) = ( k e. A |-> ( M ` B ) ) )
68 67 fveq2d 
 |-  ( ph -> ( sum^ ` ( M o. ( k e. A |-> B ) ) ) = ( sum^ ` ( k e. A |-> ( M ` B ) ) ) )
69 51 68 eqtrd 
 |-  ( ph -> ( sum^ ` ( M |` ran ( k e. A |-> B ) ) ) = ( sum^ ` ( k e. A |-> ( M ` B ) ) ) )
70 11 19 69 3eqtrd 
 |-  ( ph -> ( M ` U_ k e. A B ) = ( sum^ ` ( k e. A |-> ( M ` B ) ) ) )