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