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 bilani 
 |-  ( ( x ~<_ _om /\ Disj_ y e. x y ) -> Disj_ w e. x w )
37 36 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> Disj_ w e. x w )
38 31 33 37 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 ) ) )
39 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 ) )
40 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. { (/) } ) )
41 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 ) )
42 founiiun0 
 |-  ( e : NN -onto-> ( x u. { (/) } ) -> U. x = U_ n e. NN ( e ` n ) )
43 42 fveq2d 
 |-  ( e : NN -onto-> ( x u. { (/) } ) -> ( M ` U. x ) = ( M ` U_ n e. NN ( e ` n ) ) )
44 43 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 ) ) )
45 simplll 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> ph )
46 fof 
 |-  ( e : NN -onto-> ( x u. { (/) } ) -> e : NN --> ( x u. { (/) } ) )
47 46 adantl 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) -> e : NN --> ( x u. { (/) } ) )
48 elpwi 
 |-  ( x e. ~P dom M -> x C_ dom M )
49 48 adantl 
 |-  ( ( ph /\ x e. ~P dom M ) -> x C_ dom M )
50 5 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> dom M = S )
51 49 50 sseqtrd 
 |-  ( ( ph /\ x e. ~P dom M ) -> x C_ S )
52 0sal 
 |-  ( S e. SAlg -> (/) e. S )
53 1 52 syl 
 |-  ( ph -> (/) e. S )
54 snssi 
 |-  ( (/) e. S -> { (/) } C_ S )
55 53 54 syl 
 |-  ( ph -> { (/) } C_ S )
56 55 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> { (/) } C_ S )
57 51 56 unssd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( x u. { (/) } ) C_ S )
58 57 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) -> ( x u. { (/) } ) C_ S )
59 47 58 fssd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) -> e : NN --> S )
60 59 adantr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> e : NN --> S )
61 simpr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> Disj_ n e. NN ( e ` n ) )
62 45 60 61 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 ) ) ) ) )
63 62 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 ) ) ) ) )
64 2 feqmptd 
 |-  ( ph -> M = ( y e. S |-> ( M ` y ) ) )
65 64 reseq1d 
 |-  ( ph -> ( M |` x ) = ( ( y e. S |-> ( M ` y ) ) |` x ) )
66 65 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( M |` x ) = ( ( y e. S |-> ( M ` y ) ) |` x ) )
67 66 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( M |` x ) = ( ( y e. S |-> ( M ` y ) ) |` x ) )
68 51 resmptd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( y e. S |-> ( M ` y ) ) |` x ) = ( y e. x |-> ( M ` y ) ) )
69 68 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( ( y e. S |-> ( M ` y ) ) |` x ) = ( y e. x |-> ( M ` y ) ) )
70 snssi 
 |-  ( (/) e. x -> { (/) } C_ x )
71 ssequn2 
 |-  ( { (/) } C_ x <-> ( x u. { (/) } ) = x )
72 70 71 sylib 
 |-  ( (/) e. x -> ( x u. { (/) } ) = x )
73 72 eqcomd 
 |-  ( (/) e. x -> x = ( x u. { (/) } ) )
74 73 mpteq1d 
 |-  ( (/) e. x -> ( y e. x |-> ( M ` y ) ) = ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) )
75 74 adantl 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( y e. x |-> ( M ` y ) ) = ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) )
76 67 69 75 3eqtrd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( M |` x ) = ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) )
77 76 fveq2d 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ (/) e. x ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
78 nfv 
 |-  F/ y ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x )
79 simplr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> x e. ~P dom M )
80 p0ex 
 |-  { (/) } e. _V
81 80 a1i 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> { (/) } e. _V )
82 disjsn 
 |-  ( ( x i^i { (/) } ) = (/) <-> -. (/) e. x )
83 82 bilanri 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( x i^i { (/) } ) = (/) )
84 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. x ) -> M : S --> ( 0 [,] +oo ) )
85 51 sselda 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. x ) -> y e. S )
86 84 85 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. x ) -> ( M ` y ) e. ( 0 [,] +oo ) )
87 86 adantlr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) /\ y e. x ) -> ( M ` y ) e. ( 0 [,] +oo ) )
88 elsni 
 |-  ( y e. { (/) } -> y = (/) )
89 88 fveq2d 
 |-  ( y e. { (/) } -> ( M ` y ) = ( M ` (/) ) )
90 89 adantl 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` y ) = ( M ` (/) ) )
91 2 53 ffvelcdmd 
 |-  ( ph -> ( M ` (/) ) e. ( 0 [,] +oo ) )
92 91 adantr 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` (/) ) e. ( 0 [,] +oo ) )
93 90 92 eqeltrd 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` y ) e. ( 0 [,] +oo ) )
94 93 ad4ant14 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) /\ y e. { (/) } ) -> ( M ` y ) e. ( 0 [,] +oo ) )
95 78 79 81 83 87 94 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 ) ) ) ) )
96 fveq2 
 |-  ( y = (/) -> ( M ` y ) = ( M ` (/) ) )
97 96 adantl 
 |-  ( ( ph /\ y = (/) ) -> ( M ` y ) = ( M ` (/) ) )
98 3 adantr 
 |-  ( ( ph /\ y = (/) ) -> ( M ` (/) ) = 0 )
99 97 98 eqtrd 
 |-  ( ( ph /\ y = (/) ) -> ( M ` y ) = 0 )
100 88 99 sylan2 
 |-  ( ( ph /\ y e. { (/) } ) -> ( M ` y ) = 0 )
101 100 mpteq2dva 
 |-  ( ph -> ( y e. { (/) } |-> ( M ` y ) ) = ( y e. { (/) } |-> 0 ) )
102 101 fveq2d 
 |-  ( ph -> ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) = ( sum^ ` ( y e. { (/) } |-> 0 ) ) )
103 nfv 
 |-  F/ y ph
104 80 a1i 
 |-  ( ph -> { (/) } e. _V )
105 103 104 sge0z 
 |-  ( ph -> ( sum^ ` ( y e. { (/) } |-> 0 ) ) = 0 )
106 102 105 eqtrd 
 |-  ( ph -> ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) = 0 )
107 106 oveq2d 
 |-  ( ph -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e ( sum^ ` ( y e. { (/) } |-> ( M ` y ) ) ) ) = ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) )
108 107 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 ) )
109 simpr 
 |-  ( ( ph /\ x e. ~P dom M ) -> x e. ~P dom M )
110 66 68 eqtrd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( M |` x ) = ( y e. x |-> ( M ` y ) ) )
111 2 adantr 
 |-  ( ( ph /\ x e. ~P dom M ) -> M : S --> ( 0 [,] +oo ) )
112 111 51 fssresd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( M |` x ) : x --> ( 0 [,] +oo ) )
113 110 112 feq1dd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( y e. x |-> ( M ` y ) ) : x --> ( 0 [,] +oo ) )
114 109 113 sge0xrcl 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( y e. x |-> ( M ` y ) ) ) e. RR* )
115 114 xaddridd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) = ( sum^ ` ( y e. x |-> ( M ` y ) ) ) )
116 110 fveq2d 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. x |-> ( M ` y ) ) ) )
117 116 eqcomd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( y e. x |-> ( M ` y ) ) ) = ( sum^ ` ( M |` x ) ) )
118 115 117 eqtrd 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) = ( sum^ ` ( M |` x ) ) )
119 118 adantr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( ( sum^ ` ( y e. x |-> ( M ` y ) ) ) +e 0 ) = ( sum^ ` ( M |` x ) ) )
120 95 108 119 3eqtrrd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ -. (/) e. x ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
121 77 120 pm2.61dan 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( sum^ ` ( M |` x ) ) = ( sum^ ` ( y e. ( x u. { (/) } ) |-> ( M ` y ) ) ) )
122 121 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 ) ) ) )
123 nfv 
 |-  F/ y ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) )
124 nfv 
 |-  F/ n ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) )
125 nfdisj1 
 |-  F/ n Disj_ n e. NN ( e ` n )
126 124 125 nfan 
 |-  F/ n ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) )
127 fveq2 
 |-  ( y = ( e ` n ) -> ( M ` y ) = ( M ` ( e ` n ) ) )
128 nnex 
 |-  NN e. _V
129 128 a1i 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> NN e. _V )
130 simplr 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) -> e : NN -onto-> ( x u. { (/) } ) )
131 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 ) )
132 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. ( x u. { (/) } ) ) -> M : S --> ( 0 [,] +oo ) )
133 57 sselda 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. ( x u. { (/) } ) ) -> y e. S )
134 132 133 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ y e. ( x u. { (/) } ) ) -> ( M ` y ) e. ( 0 [,] +oo ) )
135 134 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 ) )
136 45 99 sylan 
 |-  ( ( ( ( ( ph /\ x e. ~P dom M ) /\ e : NN -onto-> ( x u. { (/) } ) ) /\ Disj_ n e. NN ( e ` n ) ) /\ y = (/) ) -> ( M ` y ) = 0 )
137 123 126 127 129 130 61 131 135 136 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 ) ) ) ) )
138 122 137 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 ) ) )
139 138 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 ) ) )
140 44 63 139 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 ) ) )
141 39 40 41 140 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 ) ) )
142 141 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 ) ) ) )
143 142 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 ) ) ) )
144 30 38 143 sylc 
 |-  ( ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ -. x = (/) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
145 27 144 pm2.61dan 
 |-  ( ( ( ph /\ x e. ~P dom M ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) )
146 145 ex 
 |-  ( ( ph /\ x e. ~P dom M ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
147 146 ralrimiva 
 |-  ( ph -> A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
148 9 3 147 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 ) ) ) ) )
149 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 ) ) ) ) )
150 148 149 sylibr 
 |-  ( ph -> M e. Meas )