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 kφ
meadjiun.m φMMeas
meadjiun.s S=domM
meadjiun.b φkABS
meadjiun.a φAω
meadjiun.dj φDisjkAB
Assertion meadjiun φMkAB=sum^kAMB

Proof

Step Hyp Ref Expression
1 meadjiun.1 kφ
2 meadjiun.m φMMeas
3 meadjiun.s S=domM
4 meadjiun.b φkABS
5 meadjiun.a φAω
6 meadjiun.dj φDisjkAB
7 4 ex φkABS
8 1 7 ralrimi φkABS
9 dfiun3g kABSkAB=rankAB
10 8 9 syl φkAB=rankAB
11 10 fveq2d φMkAB=MrankAB
12 eqid kAB=kAB
13 1 12 4 rnmptssd φrankABS
14 1stcrestlem AωrankABω
15 5 14 syl φrankABω
16 12 disjrnmpt2 DisjkABDisjxrankABx
17 6 16 syl φDisjxrankABx
18 2 3 13 15 17 meadjuni φMrankAB=sum^MrankAB
19 reldom Rel
20 brrelex1 RelAωAV
21 19 20 mpan AωAV
22 5 21 syl φAV
23 1 4 12 fmptdf φkAB:AS
24 fveq2 j=ikABj=kABi
25 24 neeq1d j=ikABjkABi
26 25 cbvrabv jA|kABj=iA|kABi
27 simpr φiAiA
28 nfv kiA
29 1 28 nfan kφiA
30 nfcv _ki
31 30 nfcsb1 _ki/kB
32 nfcv _kS
33 31 32 nfel ki/kBS
34 29 33 nfim kφiAi/kBS
35 eleq1w k=ikAiA
36 35 anbi2d k=iφkAφiA
37 csbeq1a k=iB=i/kB
38 37 eleq1d k=iBSi/kBS
39 36 38 imbi12d k=iφkABSφiAi/kBS
40 34 39 4 chvarfv φiAi/kBS
41 30 31 37 12 fvmptf iAi/kBSkABi=i/kB
42 27 40 41 syl2anc φiAkABi=i/kB
43 42 disjeq2dv φDisjiAkABiDisjiAi/kB
44 nfcv _iB
45 44 31 37 cbvdisj DisjkABDisjiAi/kB
46 45 bicomi DisjiAi/kBDisjkAB
47 46 a1i φDisjiAi/kBDisjkAB
48 43 47 bitrd φDisjiAkABiDisjkAB
49 6 48 mpbird φDisjiAkABi
50 2 3 22 23 26 49 meadjiunlem φsum^MrankAB=sum^MkAB
51 44 31 37 cbvmpt kAB=iAi/kB
52 51 coeq2i MkAB=MiAi/kB
53 52 a1i φMkAB=MiAi/kB
54 eqidd φiAi/kB=iAi/kB
55 2 3 meaf φM:S0+∞
56 55 feqmptd φM=ySMy
57 fveq2 y=i/kBMy=Mi/kB
58 40 54 56 57 fmptco φMiAi/kB=iAMi/kB
59 nfcv _iMB
60 nfcv _kM
61 60 31 nffv _kMi/kB
62 37 fveq2d k=iMB=Mi/kB
63 59 61 62 cbvmpt kAMB=iAMi/kB
64 63 eqcomi iAMi/kB=kAMB
65 64 a1i φiAMi/kB=kAMB
66 53 58 65 3eqtrd φMkAB=kAMB
67 66 fveq2d φsum^MkAB=sum^kAMB
68 50 67 eqtrd φsum^MrankAB=sum^kAMB
69 11 18 68 3eqtrd φMkAB=sum^kAMB