Metamath Proof Explorer

Theorem meadjun

Description: The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses meadjun.m 
|- ( ph -> M e. Meas )
meadjun.x 
|- S = dom M
meadjun.a 
|- ( ph -> A e. S )
meadjun.b 
|- ( ph -> B e. S )
meadjun.dj 
|- ( ph -> ( A i^i B ) = (/) )
Assertion meadjun 
|- ( ph -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )

Proof

Step Hyp Ref Expression
1 meadjun.m 
 |-  ( ph -> M e. Meas )
2 meadjun.x 
 |-  S = dom M
3 meadjun.a 
 |-  ( ph -> A e. S )
4 meadjun.b 
 |-  ( ph -> B e. S )
5 meadjun.dj 
 |-  ( ph -> ( A i^i B ) = (/) )
6 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
7 1 2 meaf 
 |-  ( ph -> M : S --> ( 0 [,] +oo ) )
8 7 4 ffvelrnd 
 |-  ( ph -> ( M ` B ) e. ( 0 [,] +oo ) )
9 6 8 sseldi 
 |-  ( ph -> ( M ` B ) e. RR* )
10 xaddid2 
 |-  ( ( M ` B ) e. RR* -> ( 0 +e ( M ` B ) ) = ( M ` B ) )
11 9 10 syl 
 |-  ( ph -> ( 0 +e ( M ` B ) ) = ( M ` B ) )
12 11 eqcomd 
 |-  ( ph -> ( M ` B ) = ( 0 +e ( M ` B ) ) )
13 12 adantr 
 |-  ( ( ph /\ A = (/) ) -> ( M ` B ) = ( 0 +e ( M ` B ) ) )
14 uneq1 
 |-  ( A = (/) -> ( A u. B ) = ( (/) u. B ) )
15 0un 
 |-  ( (/) u. B ) = B
16 15 a1i 
 |-  ( A = (/) -> ( (/) u. B ) = B )
17 14 16 eqtrd 
 |-  ( A = (/) -> ( A u. B ) = B )
18 17 fveq2d 
 |-  ( A = (/) -> ( M ` ( A u. B ) ) = ( M ` B ) )
19 18 adantl 
 |-  ( ( ph /\ A = (/) ) -> ( M ` ( A u. B ) ) = ( M ` B ) )
20 fveq2 
 |-  ( A = (/) -> ( M ` A ) = ( M ` (/) ) )
21 20 adantl 
 |-  ( ( ph /\ A = (/) ) -> ( M ` A ) = ( M ` (/) ) )
22 1 mea0 
 |-  ( ph -> ( M ` (/) ) = 0 )
23 22 adantr 
 |-  ( ( ph /\ A = (/) ) -> ( M ` (/) ) = 0 )
24 21 23 eqtrd 
 |-  ( ( ph /\ A = (/) ) -> ( M ` A ) = 0 )
25 24 oveq1d 
 |-  ( ( ph /\ A = (/) ) -> ( ( M ` A ) +e ( M ` B ) ) = ( 0 +e ( M ` B ) ) )
26 13 19 25 3eqtr4d 
 |-  ( ( ph /\ A = (/) ) -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )
27 simpl 
 |-  ( ( ph /\ -. A = (/) ) -> ph )
28 5 ad2antrr 
 |-  ( ( ( ph /\ -. A = (/) ) /\ A = B ) -> ( A i^i B ) = (/) )
29 inidm 
 |-  ( A i^i A ) = A
30 29 eqcomi 
 |-  A = ( A i^i A )
31 ineq2 
 |-  ( A = B -> ( A i^i A ) = ( A i^i B ) )
32 30 31 syl5req 
 |-  ( A = B -> ( A i^i B ) = A )
33 32 adantl 
 |-  ( ( -. A = (/) /\ A = B ) -> ( A i^i B ) = A )
34 neqne 
 |-  ( -. A = (/) -> A =/= (/) )
35 34 adantr 
 |-  ( ( -. A = (/) /\ A = B ) -> A =/= (/) )
36 33 35 eqnetrd 
 |-  ( ( -. A = (/) /\ A = B ) -> ( A i^i B ) =/= (/) )
37 36 neneqd 
 |-  ( ( -. A = (/) /\ A = B ) -> -. ( A i^i B ) = (/) )
38 37 adantll 
 |-  ( ( ( ph /\ -. A = (/) ) /\ A = B ) -> -. ( A i^i B ) = (/) )
39 28 38 pm2.65da 
 |-  ( ( ph /\ -. A = (/) ) -> -. A = B )
40 39 neqned 
 |-  ( ( ph /\ -. A = (/) ) -> A =/= B )
41 uniprg 
 |-  ( ( A e. S /\ B e. S ) -> U. { A , B } = ( A u. B ) )
42 3 4 41 syl2anc 
 |-  ( ph -> U. { A , B } = ( A u. B ) )
43 42 eqcomd 
 |-  ( ph -> ( A u. B ) = U. { A , B } )
44 43 fveq2d 
 |-  ( ph -> ( M ` ( A u. B ) ) = ( M ` U. { A , B } ) )
45 44 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( M ` ( A u. B ) ) = ( M ` U. { A , B } ) )
46 3 4 prssd 
 |-  ( ph -> { A , B } C_ S )
47 prfi 
 |-  { A , B } e. Fin
48 isfinite 
 |-  ( { A , B } e. Fin <-> { A , B } ~< _om )
49 48 biimpi 
 |-  ( { A , B } e. Fin -> { A , B } ~< _om )
50 sdomdom 
 |-  ( { A , B } ~< _om -> { A , B } ~<_ _om )
51 49 50 syl 
 |-  ( { A , B } e. Fin -> { A , B } ~<_ _om )
52 47 51 ax-mp 
 |-  { A , B } ~<_ _om
53 52 a1i 
 |-  ( ph -> { A , B } ~<_ _om )
54 disjxsn 
 |-  Disj_ x e. { B } x
55 54 a1i 
 |-  ( A = B -> Disj_ x e. { B } x )
56 preq1 
 |-  ( A = B -> { A , B } = { B , B } )
57 dfsn2 
 |-  { B } = { B , B }
58 57 eqcomi 
 |-  { B , B } = { B }
59 58 a1i 
 |-  ( A = B -> { B , B } = { B } )
60 56 59 eqtrd 
 |-  ( A = B -> { A , B } = { B } )
61 60 disjeq1d 
 |-  ( A = B -> ( Disj_ x e. { A , B } x <-> Disj_ x e. { B } x ) )
62 55 61 mpbird 
 |-  ( A = B -> Disj_ x e. { A , B } x )
63 62 adantl 
 |-  ( ( ph /\ A = B ) -> Disj_ x e. { A , B } x )
64 simpl 
 |-  ( ( ph /\ -. A = B ) -> ph )
65 neqne 
 |-  ( -. A = B -> A =/= B )
66 65 adantl 
 |-  ( ( ph /\ -. A = B ) -> A =/= B )
67 5 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( A i^i B ) = (/) )
68 3 adantr 
 |-  ( ( ph /\ A =/= B ) -> A e. S )
69 4 adantr 
 |-  ( ( ph /\ A =/= B ) -> B e. S )
70 simpr 
 |-  ( ( ph /\ A =/= B ) -> A =/= B )
71 id 
 |-  ( x = A -> x = A )
72 id 
 |-  ( x = B -> x = B )
73 71 72 disjprg 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( Disj_ x e. { A , B } x <-> ( A i^i B ) = (/) ) )
74 68 69 70 73 syl3anc 
 |-  ( ( ph /\ A =/= B ) -> ( Disj_ x e. { A , B } x <-> ( A i^i B ) = (/) ) )
75 67 74 mpbird 
 |-  ( ( ph /\ A =/= B ) -> Disj_ x e. { A , B } x )
76 64 66 75 syl2anc 
 |-  ( ( ph /\ -. A = B ) -> Disj_ x e. { A , B } x )
77 63 76 pm2.61dan 
 |-  ( ph -> Disj_ x e. { A , B } x )
78 1 2 46 53 77 meadjuni 
 |-  ( ph -> ( M ` U. { A , B } ) = ( sum^ ` ( M |` { A , B } ) ) )
79 78 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( M ` U. { A , B } ) = ( sum^ ` ( M |` { A , B } ) ) )
80 7 3 ffvelrnd 
 |-  ( ph -> ( M ` A ) e. ( 0 [,] +oo ) )
81 80 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( M ` A ) e. ( 0 [,] +oo ) )
82 8 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( M ` B ) e. ( 0 [,] +oo ) )
83 fveq2 
 |-  ( x = A -> ( M ` x ) = ( M ` A ) )
84 fveq2 
 |-  ( x = B -> ( M ` x ) = ( M ` B ) )
85 68 69 81 82 83 84 70 sge0pr 
 |-  ( ( ph /\ A =/= B ) -> ( sum^ ` ( x e. { A , B } |-> ( M ` x ) ) ) = ( ( M ` A ) +e ( M ` B ) ) )
86 7 46 fssresd 
 |-  ( ph -> ( M |` { A , B } ) : { A , B } --> ( 0 [,] +oo ) )
87 86 feqmptd 
 |-  ( ph -> ( M |` { A , B } ) = ( x e. { A , B } |-> ( ( M |` { A , B } ) ` x ) ) )
88 fvres 
 |-  ( x e. { A , B } -> ( ( M |` { A , B } ) ` x ) = ( M ` x ) )
89 88 mpteq2ia 
 |-  ( x e. { A , B } |-> ( ( M |` { A , B } ) ` x ) ) = ( x e. { A , B } |-> ( M ` x ) )
90 89 a1i 
 |-  ( ph -> ( x e. { A , B } |-> ( ( M |` { A , B } ) ` x ) ) = ( x e. { A , B } |-> ( M ` x ) ) )
91 87 90 eqtrd 
 |-  ( ph -> ( M |` { A , B } ) = ( x e. { A , B } |-> ( M ` x ) ) )
92 91 fveq2d 
 |-  ( ph -> ( sum^ ` ( M |` { A , B } ) ) = ( sum^ ` ( x e. { A , B } |-> ( M ` x ) ) ) )
93 92 adantr 
 |-  ( ( ph /\ A =/= B ) -> ( sum^ ` ( M |` { A , B } ) ) = ( sum^ ` ( x e. { A , B } |-> ( M ` x ) ) ) )
94 eqidd 
 |-  ( ( ph /\ A =/= B ) -> ( ( M ` A ) +e ( M ` B ) ) = ( ( M ` A ) +e ( M ` B ) ) )
95 85 93 94 3eqtr4d 
 |-  ( ( ph /\ A =/= B ) -> ( sum^ ` ( M |` { A , B } ) ) = ( ( M ` A ) +e ( M ` B ) ) )
96 45 79 95 3eqtrd 
 |-  ( ( ph /\ A =/= B ) -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )
97 27 40 96 syl2anc 
 |-  ( ( ph /\ -. A = (/) ) -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )
98 26 97 pm2.61dan 
 |-  ( ph -> ( M ` ( A u. B ) ) = ( ( M ` A ) +e ( M ` B ) ) )