Metamath Proof Explorer

Theorem measdivcstALTV

Description: Alternate version of measdivcst . (Contributed by Thierry Arnoux, 25-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion measdivcstALTV 
|- ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) )

Proof

Step Hyp Ref Expression
1 funmpt 
 |-  Fun ( x e. S |-> ( ( M ` x ) /e A ) )
2 ovex 
 |-  ( ( M ` x ) /e A ) e. _V
3 2 rgenw 
 |-  A. x e. S ( ( M ` x ) /e A ) e. _V
4 dmmptg 
 |-  ( A. x e. S ( ( M ` x ) /e A ) e. _V -> dom ( x e. S |-> ( ( M ` x ) /e A ) ) = S )
5 3 4 ax-mp 
 |-  dom ( x e. S |-> ( ( M ` x ) /e A ) ) = S
6 df-fn 
 |-  ( ( x e. S |-> ( ( M ` x ) /e A ) ) Fn S <-> ( Fun ( x e. S |-> ( ( M ` x ) /e A ) ) /\ dom ( x e. S |-> ( ( M ` x ) /e A ) ) = S ) )
7 1 5 6 mpbir2an 
 |-  ( x e. S |-> ( ( M ` x ) /e A ) ) Fn S
8 7 a1i 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) Fn S )
9 vex 
 |-  y e. _V
10 eqid 
 |-  ( x e. S |-> ( ( M ` x ) /e A ) ) = ( x e. S |-> ( ( M ` x ) /e A ) )
11 10 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. S |-> ( ( M ` x ) /e A ) ) <-> E. x e. S y = ( ( M ` x ) /e A ) ) )
12 9 11 ax-mp 
 |-  ( y e. ran ( x e. S |-> ( ( M ` x ) /e A ) ) <-> E. x e. S y = ( ( M ` x ) /e A ) )
13 measfrge0 
 |-  ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )
14 ffvelrn 
 |-  ( ( M : S --> ( 0 [,] +oo ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
15 13 14 sylan 
 |-  ( ( M e. ( measures ` S ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
16 15 adantlr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
17 simplr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> A e. RR+ )
18 16 17 xrpxdivcld 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( ( M ` x ) /e A ) e. ( 0 [,] +oo ) )
19 eleq1a 
 |-  ( ( ( M ` x ) /e A ) e. ( 0 [,] +oo ) -> ( y = ( ( M ` x ) /e A ) -> y e. ( 0 [,] +oo ) ) )
20 18 19 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( y = ( ( M ` x ) /e A ) -> y e. ( 0 [,] +oo ) ) )
21 20 rexlimdva 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( E. x e. S y = ( ( M ` x ) /e A ) -> y e. ( 0 [,] +oo ) ) )
22 12 21 syl5bi 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( y e. ran ( x e. S |-> ( ( M ` x ) /e A ) ) -> y e. ( 0 [,] +oo ) ) )
23 22 ssrdv 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ran ( x e. S |-> ( ( M ` x ) /e A ) ) C_ ( 0 [,] +oo ) )
24 df-f 
 |-  ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) <-> ( ( x e. S |-> ( ( M ` x ) /e A ) ) Fn S /\ ran ( x e. S |-> ( ( M ` x ) /e A ) ) C_ ( 0 [,] +oo ) ) )
25 8 23 24 sylanbrc 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) )
26 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
27 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
28 26 27 syl 
 |-  ( M e. ( measures ` S ) -> (/) e. S )
29 28 adantr 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> (/) e. S )
30 ovex 
 |-  ( ( M ` (/) ) /e A ) e. _V
31 29 30 jctir 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( (/) e. S /\ ( ( M ` (/) ) /e A ) e. _V ) )
32 fveq2 
 |-  ( x = (/) -> ( M ` x ) = ( M ` (/) ) )
33 32 oveq1d 
 |-  ( x = (/) -> ( ( M ` x ) /e A ) = ( ( M ` (/) ) /e A ) )
34 33 10 fvmptg 
 |-  ( ( (/) e. S /\ ( ( M ` (/) ) /e A ) e. _V ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = ( ( M ` (/) ) /e A ) )
35 31 34 syl 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = ( ( M ` (/) ) /e A ) )
36 measvnul 
 |-  ( M e. ( measures ` S ) -> ( M ` (/) ) = 0 )
37 36 oveq1d 
 |-  ( M e. ( measures ` S ) -> ( ( M ` (/) ) /e A ) = ( 0 /e A ) )
38 xdiv0rp 
 |-  ( A e. RR+ -> ( 0 /e A ) = 0 )
39 37 38 sylan9eq 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( M ` (/) ) /e A ) = 0 )
40 35 39 eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 )
41 simpll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M e. ( measures ` S ) /\ A e. RR+ ) )
42 simplr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> y e. ~P S )
43 simprl 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> y ~<_ _om )
44 simprr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> Disj_ z e. y z )
45 42 43 44 3jca 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) )
46 9 a1i 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> y e. _V )
47 simplll 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> M e. ( measures ` S ) )
48 simplr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> y e. ~P S )
49 simpr 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> z e. y )
50 elpwg 
 |-  ( y e. _V -> ( y e. ~P S <-> y C_ S ) )
51 9 50 ax-mp 
 |-  ( y e. ~P S <-> y C_ S )
52 ssel2 
 |-  ( ( y C_ S /\ z e. y ) -> z e. S )
53 51 52 sylanb 
 |-  ( ( y e. ~P S /\ z e. y ) -> z e. S )
54 48 49 53 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> z e. S )
55 measvxrge0 
 |-  ( ( M e. ( measures ` S ) /\ z e. S ) -> ( M ` z ) e. ( 0 [,] +oo ) )
56 47 54 55 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> ( M ` z ) e. ( 0 [,] +oo ) )
57 simplr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> A e. RR+ )
58 46 56 57 esumdivc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> ( sum* z e. y ( M ` z ) /e A ) = sum* z e. y ( ( M ` z ) /e A ) )
59 58 3ad2antr1 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( sum* z e. y ( M ` z ) /e A ) = sum* z e. y ( ( M ` z ) /e A ) )
60 26 ad2antrr 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> S e. U. ran sigAlgebra )
61 simpr1 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> y e. ~P S )
62 simpr2 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> y ~<_ _om )
63 sigaclcu 
 |-  ( ( S e. U. ran sigAlgebra /\ y e. ~P S /\ y ~<_ _om ) -> U. y e. S )
64 60 61 62 63 syl3anc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> U. y e. S )
65 fveq2 
 |-  ( x = U. y -> ( M ` x ) = ( M ` U. y ) )
66 65 oveq1d 
 |-  ( x = U. y -> ( ( M ` x ) /e A ) = ( ( M ` U. y ) /e A ) )
67 66 10 2 fvmpt3i 
 |-  ( U. y e. S -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = ( ( M ` U. y ) /e A ) )
68 64 67 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = ( ( M ` U. y ) /e A ) )
69 simpll 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> M e. ( measures ` S ) )
70 69 61 jca 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M e. ( measures ` S ) /\ y e. ~P S ) )
71 simpr3 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> Disj_ z e. y z )
72 62 71 jca 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( y ~<_ _om /\ Disj_ z e. y z ) )
73 measvun 
 |-  ( ( M e. ( measures ` S ) /\ y e. ~P S /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) )
74 73 3expia 
 |-  ( ( M e. ( measures ` S ) /\ y e. ~P S ) -> ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) ) )
75 74 ralrimiva 
 |-  ( M e. ( measures ` S ) -> A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) ) )
76 75 r19.21bi 
 |-  ( ( M e. ( measures ` S ) /\ y e. ~P S ) -> ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) ) )
77 70 72 76 sylc 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( M ` U. y ) = sum* z e. y ( M ` z ) )
78 77 oveq1d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( M ` U. y ) /e A ) = ( sum* z e. y ( M ` z ) /e A ) )
79 68 78 eqtrd 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = ( sum* z e. y ( M ` z ) /e A ) )
80 fveq2 
 |-  ( x = z -> ( M ` x ) = ( M ` z ) )
81 80 oveq1d 
 |-  ( x = z -> ( ( M ` x ) /e A ) = ( ( M ` z ) /e A ) )
82 81 10 2 fvmpt3i 
 |-  ( z e. S -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = ( ( M ` z ) /e A ) )
83 53 82 syl 
 |-  ( ( y e. ~P S /\ z e. y ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = ( ( M ` z ) /e A ) )
84 83 esumeq2dv 
 |-  ( y e. ~P S -> sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = sum* z e. y ( ( M ` z ) /e A ) )
85 61 84 syl 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) = sum* z e. y ( ( M ` z ) /e A ) )
86 59 79 85 3eqtr4d 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) )
87 41 45 86 syl2anc 
 |-  ( ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ _om /\ Disj_ z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) )
88 87 ex 
 |-  ( ( ( M e. ( measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) )
89 88 ralrimiva 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) )
90 25 40 89 3jca 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) )
91 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) <-> ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) ) )
92 26 91 syl 
 |-  ( M e. ( measures ` S ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) <-> ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) ) )
93 92 biimprd 
 |-  ( M e. ( measures ` S ) -> ( ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) ) )
94 93 adantr 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( ( ( x e. S |-> ( ( M ` x ) /e A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ _om /\ Disj_ z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` U. y ) = sum* z e. y ( ( x e. S |-> ( ( M ` x ) /e A ) ) ` z ) ) ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) ) )
95 90 94 mpd 
 |-  ( ( M e. ( measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /e A ) ) e. ( measures ` S ) )