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 ) ) ) |