Metamath Proof Explorer

Theorem ismeannd

Description: Sufficient condition to prove that M is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses ismeannd.sal 
|- ( ph -> S e. SAlg )
ismeannd.mf 
|- ( ph -> M : S --> ( 0 [,] +oo ) )
ismeannd.m0 
|- ( ph -> ( M ` (/) ) = 0 )
ismeannd.iun 
|- ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) )
Assertion ismeannd 
|- ( ph -> M e. Meas )

Proof

Step Hyp Ref Expression
1 ismeannd.sal 
 |-  ( ph -> S e. SAlg )
2 ismeannd.mf 
 |-  ( ph -> M : S --> ( 0 [,] +oo ) )
3 ismeannd.m0 
 |-  ( ph -> ( M ` (/) ) = 0 )
4 ismeannd.iun 
 |-  ( ( ph /\ e : NN --> S /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) )
5 2 fdmd 
 |-  ( ph -> dom M = S )
6 5 feq2d 
 |-  ( ph -> ( M : dom M --> ( 0 [,] +oo ) <-> M : S --> ( 0 [,] +oo ) ) )
7 2 6 mpbird 
 |-  ( ph -> M : dom M --> ( 0 [,] +oo ) )
8 5 1 eqeltrd 
 |-  ( ph -> dom M e. SAlg )
9 7 8 jca 
 |-  ( ph -> ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) )
10 unieq 
 |-  ( x = (/) -> U. x = U. (/) )
11 uni0 
 |-  U. (/) = (/)
12 11 a1i 
 |-  ( x = (/) -> U. (/) = (/) )
13 10 12 eqtrd 
 |-  ( x = (/) -> U. x = (/) )
14 13 fveq2d 
 |-  ( x = (/) -> ( M ` U. x ) = ( M ` (/) ) )
15 14 3 sylan9eqr 
 |-  ( ( ph /\ x = (/) ) -> ( M ` U. x ) = 0 )
16 reseq2 
 |-  ( x = (/) -> ( M |` x ) = ( M |` (/) ) )
17 res0 
 |-  ( M |` (/) ) = (/)
18 17 a1i 
 |-  ( x = (/) -> ( M |` (/) ) = (/) )
19 16 18 eqtrd 
 |-  ( x = (/) -> ( M |` x ) = (/) )
20 19 fveq2d 
 |-  ( x = (/) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` (/) ) )
21 20 adantl 
 |-  ( ( ph /\ x = (/) ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` (/) ) )
22 sge00 
 |-  ( sum^ ` (/) ) = 0
23 22 a1i 
 |-  ( ( ph /\ x = (/) ) -> ( sum^ ` (/) ) = 0 )
24 21 23 eqtrd 
 |-  ( ( ph /\ x = (/) ) -> ( sum^ ` ( M |` x ) ) = 0 )
25 15 24 eqtr4d 
 |-  ( ( ph /\ x = (/) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
26 25 adantlr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ x = (/) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
27 26 adantlr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ x = (/) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
28 simpll 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> ( ph /\ x e. ~P dom M ) )
29 simplrr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> Disj_ y e. x y )
30 28 29 jca 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) )
31 simplrl 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> x ~<_ _om )
32 neqne 
 |-  ( -. x = (/) -> x =/= (/) )
33 32 adantl 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> x =/= (/) )
34 id 
 |-  ( y = w -> y = w )
35 34 cbvdisjv 
 |-  ( Disj_ y e. x y <-> Disj_ w e. x w )
36 35 biimpi 
 |-  ( Disj_ y e. x y -> Disj_ w e. x w )
37 36 adantl 
 |-  ( ( x ~<_ _om /\ Disj_ y e. x y ) -> Disj_ w e. x w )
38 37 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> Disj_ w e. x w )
39 31 33 38 nnfoctbdj 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> E. e ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) )
40 simpl 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) ) -> ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) )
41 simprl 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) ) -> e : NN -onto-> ( x u. { (/) } ) )
42 simprr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) ) -> Disj_ n e. NN ( e ` n ) )
43 founiiun0 
 |-  ( e : NN -onto-> ( x u. { (/) } ) -> U. x = U_ n e. NN ( e ` n ) )
44 43 fveq2d 
 |-  ( e : NN -onto-> ( x u. { (/) } ) -> ( M ` U. x ) = ( M ` U_ n e. NN ( e ` n ) ) )
45 44 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U. x ) = ( M ` U_ n e. NN ( e ` n ) ) )
46 simplll 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ph )
47 fof 
 |-  ( e : NN -onto-> ( x u. { (/) } ) -> e : NN --> ( x u. { (/) } ) )
48 47 adantl 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) -> e : NN --> ( x u. { (/) } ) )
49 elpwi 
 |-  ( x e. ~P dom M -> x C_ dom M )
50 49 adantl 
 |-  ( ( ph /\ x e. ~P dom M ) -> x C_ dom M )
51 5 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> dom M = S )
52 50 51 sseqtrd 
 |-  ( ( ph /\ x e. ~P dom M ) -> x C_ S )
53 0sal 
 |-  ( S e. SAlg -> (/) e. S )
54 1 53 syl 
 |-  ( ph -> (/) e. S )
55 snssi 
 |-  ( (/) e. S -> { (/) } C_ S )
56 54 55 syl 
 |-  ( ph -> { (/) } C_ S )
57 56 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> { (/) } C_ S )
58 52 57 unssd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( x u. { (/) } ) C_ S )
59 58 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) -> ( x u. { (/) } ) C_ S )
60 48 59 fssd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) -> e : NN --> S )
61 60 adantr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> e : NN --> S )
62 simpr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> Disj_ n e. NN ( e ` n ) )
63 46 61 62 4 syl3anc 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) )
64 63 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U_ n e. NN ( e ` n ) ) = ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) )
65 2 feqmptd 
 |-  ( ph -> M = ( y e. S |-> ( M ` y ) ) )
66 65 reseq1d 
 |-  ( ph -> ( M |` x ) = ( ( y e. S |-> ( M ` y ) ) |` x ) )
67 66 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( M |` x ) = ( ( y e. S |-> ( M ` y ) ) |` x ) )
68 67 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( M |` x ) = ( ( y e. S |-> ( M ` y ) ) |` x ) )
69 52 resmptd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( y e. S |-> ( M ` y ) ) |` x ) = ( y e. x |-> ( M ` y ) ) )
70 69 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( ( y e. S |-> ( M ` y ) ) |` x ) = ( y e. x |-> ( M ` y ) ) )
71 snssi 
 |-  ( (/) e. x -> { (/) } C_ x )
72 ssequn2 
 |-  ( { (/) } C_ x <-> ( x u. { (/) } ) = x )
73 71 72 sylib 
 |-  ( (/) e. x -> ( x u. { (/) } ) = x )
74 73 eqcomd 
 |-  ( (/) e. x -> x = ( x u. { (/) } ) )
75 74 mpteq1d 
 |-  ( (/) e. x -> ( y e. x |-> ( M ` y ) ) = ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) )
76 75 adantl 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( y e. x |-> ( M ` y ) ) = ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) )
77 68 70 76 3eqtrd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( M |` x ) = ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) )
78 77 fveq2d 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
79 nfv 
 |-  F/ y ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x )
80 simplr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> x e. ~P dom M )
81 p0ex 
 |-  { (/) } e. _V
82 81 a1i 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> { (/) } e. _V )
83 disjsn 
 |-  ( ( x i^i { (/) } ) = (/) <-> -. (/) e. x )
84 83 biimpri 
 |-  ( -. (/) e. x -> ( x i^i { (/) } ) = (/) )
85 84 adantl 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( x i^i { (/) } ) = (/) )
86 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. x ) -> M : S --> ( 0 [,] +oo ) )
87 52 sselda 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. x ) -> y e. S )
88 86 87 ffvelrnd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. x ) -> ( M ` y ) e. ( 0 [,] +oo ) )
89 88 adantlr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) /\ y e. x ) -> ( M ` y ) e. ( 0 [,] +oo ) )
90 elsni 
 |-  ( y e. { (/) } -> y = (/) )
91 90 fveq2d 
 |-  ( y e. { (/) } -> ( M ` y ) = ( M ` (/) ) )
92 91 adantl 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` y ) = ( M ` (/) ) )
93 2 54 ffvelrnd 
 |-  ( ph -> ( M ` (/) ) e. ( 0 [,] +oo ) )
94 93 adantr 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` (/) ) e. ( 0 [,] +oo ) )
95 92 94 eqeltrd 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` y ) e. ( 0 [,] +oo ) )
96 95 ad4ant14 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) /\ y e. { (/) } ) -> ( M ` y ) e. ( 0 [,] +oo ) )
97 79 80 82 85 89 96 sge0splitmpt 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) = ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) ) )
98 fveq2 
 |-  ( y = (/) -> ( M ` y ) = ( M ` (/) ) )
99 98 adantl 
 |-  ( ( ph /\ y = (/) ) -> ( M ` y ) = ( M ` (/) ) )
100 3 adantr 
 |-  ( ( ph /\ y = (/) ) -> ( M ` (/) ) = 0 )
101 99 100 eqtrd 
 |-  ( ( ph /\ y = (/) ) -> ( M ` y ) = 0 )
102 90 101 sylan2 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` y ) = 0 )
103 102 mpteq2dva 
 |-  ( ph -> ( y e. { (/) } |-> ( M ` y ) ) = ( y e. { (/) } |-> 0 ) )
104 103 fveq2d 
 |-  ( ph -> ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) = ( sum^ ` ( y e. { (/) } |-> 0 ) ) )
105 nfv 
 |-  F/ y ph
106 81 a1i 
 |-  ( ph -> { (/) } e. _V )
107 105 106 sge0z 
 |-  ( ph -> ( sum^ ` ( y e. { (/) } |-> 0 ) ) = 0 )
108 104 107 eqtrd 
 |-  ( ph -> ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) = 0 )
109 108 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) ) = ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) )
110 109 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) ) = ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) )
111 simpr 
 |-  ( ( ph /\ x e. ~P dom M ) -> x e. ~P dom M )
112 67 69 eqtrd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( M |` x ) = ( y e. x |-> ( M ` y ) ) )
113 2 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> M : S --> ( 0 [,] +oo ) )
114 113 52 fssresd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( M |` x ) : x --> ( 0 [,] +oo ) )
115 112 114 feq1dd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( y e. x |-> ( M ` y ) ) : x --> ( 0 [,] +oo ) )
116 111 115 sge0xrcl 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( y e. x |-> ( M ` y ) ) ) e. RR* )
117 116 xaddid1d 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) = ( sum^ ` ( y e. x |-> ( M ` y ) ) ) )
118 112 fveq2d 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. x |-> ( M ` y ) ) ) )
119 118 eqcomd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( y e. x |-> ( M ` y ) ) ) = ( sum^ ` ( M |` x ) ) )
120 117 119 eqtrd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) = ( sum^ ` ( M |` x ) ) )
121 120 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) = ( sum^ ` ( M |` x ) ) )
122 97 110 121 3eqtrrd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
123 78 122 pm2.61dan 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
124 123 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
125 nfv 
 |-  F/ y ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) )
126 nfv 
 |-  F/ n ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) )
127 nfdisj1 
 |-  F/ n Disj_ n e. NN ( e ` n )
128 126 127 nfan 
 |-  F/ n ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) )
129 fveq2 
 |-  ( y = ( e ` n ) -> ( M ` y ) = ( M ` ( e ` n ) ) )
130 nnex 
 |-  NN e. _V
131 130 a1i 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> NN e. _V )
132 simplr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> e : NN -onto-> ( x u. { (/) } ) )
133 eqidd 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) /\ n e. NN ) -> ( e ` n ) = ( e ` n ) )
134 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. ( x u. { (/) } ) ) -> M : S --> ( 0 [,] +oo ) )
135 58 sselda 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. ( x u. { (/) } ) ) -> y e. S )
136 134 135 ffvelrnd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. ( x u. { (/) } ) ) -> ( M ` y ) e. ( 0 [,] +oo ) )
137 136 ad4ant14 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) /\ y e. ( x u. { (/) } ) ) -> ( M ` y ) e. ( 0 [,] +oo ) )
138 46 101 sylan 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) /\ y = (/) ) -> ( M ` y ) = 0 )
139 125 128 129 131 132 62 133 137 138 sge0fodjrn 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) = ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) )
140 124 139 eqtr2d 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) = ( sum^ ` ( M |` x ) ) )
141 140 adantllr 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( sum^ ` ( n e. NN |-> ( M ` ( e ` n ) ) ) ) = ( sum^ ` ( M |` x ) ) )
142 45 64 141 3eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
143 40 41 42 142 syl21anc 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) /\ ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
144 143 ex 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) -> ( ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
145 144 exlimdv 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ Disj_ y e. x y ) -> ( E. e ( e : NN -onto-> ( x u. { (/) } ) /\ Disj_ n e. NN ( e ` n ) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
146 30 39 145 sylc 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
147 27 146 pm2.61dan 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
148 147 ex 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
149 148 ralrimiva 
 |-  ( ph -> A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
150 9 3 149 jca31 
 |-  ( ph -> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
151 ismea 
 |-  ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
152 150 151 sylibr 
 |-  ( ph -> M e. Meas )