Metamath Proof Explorer

Theorem pmeasadd

Description: A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses caraext.1 
|- ( ph -> P : R --> ( 0 [,] +oo ) )
caraext.2 
|- ( ph -> ( P ` (/) ) = 0 )
caraext.3 
|- ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) -> ( P ` U. x ) = sum* y e. x ( P ` y ) )
pmeassubadd.q 
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
pmeassubadd.1 
|- ( ph -> R e. Q )
pmeassubadd.2 
|- ( ph -> A ~<_ _om )
pmeassubadd.3 
|- ( ( ph /\ k e. A ) -> B e. R )
pmeasadd.4 
|- ( ph -> Disj_ k e. A B )
Assertion pmeasadd 
|- ( ph -> ( P ` U_ k e. A B ) = sum* k e. A ( P ` B ) )

Proof

Step Hyp Ref Expression
1 caraext.1 
 |-  ( ph -> P : R --> ( 0 [,] +oo ) )
2 caraext.2 
 |-  ( ph -> ( P ` (/) ) = 0 )
3 caraext.3 
 |-  ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) -> ( P ` U. x ) = sum* y e. x ( P ` y ) )
4 pmeassubadd.q 
 |-  Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
5 pmeassubadd.1 
 |-  ( ph -> R e. Q )
6 pmeassubadd.2 
 |-  ( ph -> A ~<_ _om )
7 pmeassubadd.3 
 |-  ( ( ph /\ k e. A ) -> B e. R )
8 pmeasadd.4 
 |-  ( ph -> Disj_ k e. A B )
9 7 ralrimiva 
 |-  ( ph -> A. k e. A B e. R )
10 dfiun3g 
 |-  ( A. k e. A B e. R -> U_ k e. A B = U. ran ( k e. A |-> B ) )
11 9 10 syl 
 |-  ( ph -> U_ k e. A B = U. ran ( k e. A |-> B ) )
12 11 fveq2d 
 |-  ( ph -> ( P ` U_ k e. A B ) = ( P ` U. ran ( k e. A |-> B ) ) )
13 mptct 
 |-  ( A ~<_ _om -> ( k e. A |-> B ) ~<_ _om )
14 rnct 
 |-  ( ( k e. A |-> B ) ~<_ _om -> ran ( k e. A |-> B ) ~<_ _om )
15 6 13 14 3syl 
 |-  ( ph -> ran ( k e. A |-> B ) ~<_ _om )
16 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
17 16 rnmptss 
 |-  ( A. k e. A B e. R -> ran ( k e. A |-> B ) C_ R )
18 9 17 syl 
 |-  ( ph -> ran ( k e. A |-> B ) C_ R )
19 disjrnmpt 
 |-  ( Disj_ k e. A B -> Disj_ y e. ran ( k e. A |-> B ) y )
20 8 19 syl 
 |-  ( ph -> Disj_ y e. ran ( k e. A |-> B ) y )
21 15 18 20 3jca 
 |-  ( ph -> ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) )
22 21 ancli 
 |-  ( ph -> ( ph /\ ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) ) )
23 ctex 
 |-  ( A ~<_ _om -> A e. _V )
24 mptexg 
 |-  ( A e. _V -> ( k e. A |-> B ) e. _V )
25 6 23 24 3syl 
 |-  ( ph -> ( k e. A |-> B ) e. _V )
26 rnexg 
 |-  ( ( k e. A |-> B ) e. _V -> ran ( k e. A |-> B ) e. _V )
27 breq1 
 |-  ( x = ran ( k e. A |-> B ) -> ( x ~<_ _om <-> ran ( k e. A |-> B ) ~<_ _om ) )
28 sseq1 
 |-  ( x = ran ( k e. A |-> B ) -> ( x C_ R <-> ran ( k e. A |-> B ) C_ R ) )
29 disjeq1 
 |-  ( x = ran ( k e. A |-> B ) -> ( Disj_ y e. x y <-> Disj_ y e. ran ( k e. A |-> B ) y ) )
30 27 28 29 3anbi123d 
 |-  ( x = ran ( k e. A |-> B ) -> ( ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) <-> ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) ) )
31 30 anbi2d 
 |-  ( x = ran ( k e. A |-> B ) -> ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) <-> ( ph /\ ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) ) ) )
32 unieq 
 |-  ( x = ran ( k e. A |-> B ) -> U. x = U. ran ( k e. A |-> B ) )
33 32 fveq2d 
 |-  ( x = ran ( k e. A |-> B ) -> ( P ` U. x ) = ( P ` U. ran ( k e. A |-> B ) ) )
34 esumeq1 
 |-  ( x = ran ( k e. A |-> B ) -> sum* y e. x ( P ` y ) = sum* y e. ran ( k e. A |-> B ) ( P ` y ) )
35 33 34 eqeq12d 
 |-  ( x = ran ( k e. A |-> B ) -> ( ( P ` U. x ) = sum* y e. x ( P ` y ) <-> ( P ` U. ran ( k e. A |-> B ) ) = sum* y e. ran ( k e. A |-> B ) ( P ` y ) ) )
36 31 35 imbi12d 
 |-  ( x = ran ( k e. A |-> B ) -> ( ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) -> ( P ` U. x ) = sum* y e. x ( P ` y ) ) <-> ( ( ph /\ ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) ) -> ( P ` U. ran ( k e. A |-> B ) ) = sum* y e. ran ( k e. A |-> B ) ( P ` y ) ) ) )
37 36 3 vtoclg 
 |-  ( ran ( k e. A |-> B ) e. _V -> ( ( ph /\ ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) ) -> ( P ` U. ran ( k e. A |-> B ) ) = sum* y e. ran ( k e. A |-> B ) ( P ` y ) ) )
38 25 26 37 3syl 
 |-  ( ph -> ( ( ph /\ ( ran ( k e. A |-> B ) ~<_ _om /\ ran ( k e. A |-> B ) C_ R /\ Disj_ y e. ran ( k e. A |-> B ) y ) ) -> ( P ` U. ran ( k e. A |-> B ) ) = sum* y e. ran ( k e. A |-> B ) ( P ` y ) ) )
39 22 38 mpd 
 |-  ( ph -> ( P ` U. ran ( k e. A |-> B ) ) = sum* y e. ran ( k e. A |-> B ) ( P ` y ) )
40 fveq2 
 |-  ( y = B -> ( P ` y ) = ( P ` B ) )
41 6 23 syl 
 |-  ( ph -> A e. _V )
42 1 adantr 
 |-  ( ( ph /\ k e. A ) -> P : R --> ( 0 [,] +oo ) )
43 42 7 ffvelrnd 
 |-  ( ( ph /\ k e. A ) -> ( P ` B ) e. ( 0 [,] +oo ) )
44 fveq2 
 |-  ( B = (/) -> ( P ` B ) = ( P ` (/) ) )
45 44 adantl 
 |-  ( ( ( ph /\ k e. A ) /\ B = (/) ) -> ( P ` B ) = ( P ` (/) ) )
46 2 ad2antrr 
 |-  ( ( ( ph /\ k e. A ) /\ B = (/) ) -> ( P ` (/) ) = 0 )
47 45 46 eqtrd 
 |-  ( ( ( ph /\ k e. A ) /\ B = (/) ) -> ( P ` B ) = 0 )
48 40 41 43 7 47 8 esumrnmpt2 
 |-  ( ph -> sum* y e. ran ( k e. A |-> B ) ( P ` y ) = sum* k e. A ( P ` B ) )
49 12 39 48 3eqtrd 
 |-  ( ph -> ( P ` U_ k e. A B ) = sum* k e. A ( P ` B ) )