Step |
Hyp |
Ref |
Expression |
1 |
|
meadjiunlem.f |
|- ( ph -> M e. Meas ) |
2 |
|
meadjiunlem.3 |
|- S = dom M |
3 |
|
meadjiunlem.x |
|- ( ph -> X e. V ) |
4 |
|
meadjiunlem.g |
|- ( ph -> G : X --> S ) |
5 |
|
meadjiunlem.y |
|- Y = { i e. X | ( G ` i ) =/= (/) } |
6 |
|
meadjiunlem.dj |
|- ( ph -> Disj_ i e. X ( G ` i ) ) |
7 |
|
nfv |
|- F/ k ph |
8 |
4 3
|
jca |
|- ( ph -> ( G : X --> S /\ X e. V ) ) |
9 |
|
fex |
|- ( ( G : X --> S /\ X e. V ) -> G e. _V ) |
10 |
|
rnexg |
|- ( G e. _V -> ran G e. _V ) |
11 |
8 9 10
|
3syl |
|- ( ph -> ran G e. _V ) |
12 |
|
difssd |
|- ( ph -> ( ran G \ { (/) } ) C_ ran G ) |
13 |
1 2
|
meaf |
|- ( ph -> M : S --> ( 0 [,] +oo ) ) |
14 |
13
|
adantr |
|- ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> M : S --> ( 0 [,] +oo ) ) |
15 |
4
|
frnd |
|- ( ph -> ran G C_ S ) |
16 |
15
|
adantr |
|- ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> ran G C_ S ) |
17 |
12
|
sselda |
|- ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> k e. ran G ) |
18 |
16 17
|
sseldd |
|- ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> k e. S ) |
19 |
14 18
|
ffvelrnd |
|- ( ( ph /\ k e. ( ran G \ { (/) } ) ) -> ( M ` k ) e. ( 0 [,] +oo ) ) |
20 |
|
simpl |
|- ( ( ph /\ k e. ( ran G \ ( ran G \ { (/) } ) ) ) -> ph ) |
21 |
|
id |
|- ( k e. ( ran G \ ( ran G \ { (/) } ) ) -> k e. ( ran G \ ( ran G \ { (/) } ) ) ) |
22 |
|
dfin4 |
|- ( ran G i^i { (/) } ) = ( ran G \ ( ran G \ { (/) } ) ) |
23 |
22
|
eqcomi |
|- ( ran G \ ( ran G \ { (/) } ) ) = ( ran G i^i { (/) } ) |
24 |
21 23
|
eleqtrdi |
|- ( k e. ( ran G \ ( ran G \ { (/) } ) ) -> k e. ( ran G i^i { (/) } ) ) |
25 |
|
elinel2 |
|- ( k e. ( ran G i^i { (/) } ) -> k e. { (/) } ) |
26 |
|
elsni |
|- ( k e. { (/) } -> k = (/) ) |
27 |
25 26
|
syl |
|- ( k e. ( ran G i^i { (/) } ) -> k = (/) ) |
28 |
24 27
|
syl |
|- ( k e. ( ran G \ ( ran G \ { (/) } ) ) -> k = (/) ) |
29 |
28
|
adantl |
|- ( ( ph /\ k e. ( ran G \ ( ran G \ { (/) } ) ) ) -> k = (/) ) |
30 |
|
simpr |
|- ( ( ph /\ k = (/) ) -> k = (/) ) |
31 |
30
|
fveq2d |
|- ( ( ph /\ k = (/) ) -> ( M ` k ) = ( M ` (/) ) ) |
32 |
1
|
mea0 |
|- ( ph -> ( M ` (/) ) = 0 ) |
33 |
32
|
adantr |
|- ( ( ph /\ k = (/) ) -> ( M ` (/) ) = 0 ) |
34 |
31 33
|
eqtrd |
|- ( ( ph /\ k = (/) ) -> ( M ` k ) = 0 ) |
35 |
20 29 34
|
syl2anc |
|- ( ( ph /\ k e. ( ran G \ ( ran G \ { (/) } ) ) ) -> ( M ` k ) = 0 ) |
36 |
7 11 12 19 35
|
sge0ss |
|- ( ph -> ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) = ( sum^ ` ( k e. ran G |-> ( M ` k ) ) ) ) |
37 |
36
|
eqcomd |
|- ( ph -> ( sum^ ` ( k e. ran G |-> ( M ` k ) ) ) = ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) ) |
38 |
13 15
|
feqresmpt |
|- ( ph -> ( M |` ran G ) = ( k e. ran G |-> ( M ` k ) ) ) |
39 |
38
|
fveq2d |
|- ( ph -> ( sum^ ` ( M |` ran G ) ) = ( sum^ ` ( k e. ran G |-> ( M ` k ) ) ) ) |
40 |
4
|
ffvelrnda |
|- ( ( ph /\ j e. X ) -> ( G ` j ) e. S ) |
41 |
4
|
feqmptd |
|- ( ph -> G = ( j e. X |-> ( G ` j ) ) ) |
42 |
13
|
feqmptd |
|- ( ph -> M = ( k e. S |-> ( M ` k ) ) ) |
43 |
|
fveq2 |
|- ( k = ( G ` j ) -> ( M ` k ) = ( M ` ( G ` j ) ) ) |
44 |
40 41 42 43
|
fmptco |
|- ( ph -> ( M o. G ) = ( j e. X |-> ( M ` ( G ` j ) ) ) ) |
45 |
44
|
fveq2d |
|- ( ph -> ( sum^ ` ( M o. G ) ) = ( sum^ ` ( j e. X |-> ( M ` ( G ` j ) ) ) ) ) |
46 |
|
nfv |
|- F/ j ph |
47 |
|
ssrab2 |
|- { i e. X | ( G ` i ) =/= (/) } C_ X |
48 |
47
|
a1i |
|- ( ph -> { i e. X | ( G ` i ) =/= (/) } C_ X ) |
49 |
5 48
|
eqsstrid |
|- ( ph -> Y C_ X ) |
50 |
13
|
adantr |
|- ( ( ph /\ j e. Y ) -> M : S --> ( 0 [,] +oo ) ) |
51 |
4
|
adantr |
|- ( ( ph /\ j e. Y ) -> G : X --> S ) |
52 |
49
|
sselda |
|- ( ( ph /\ j e. Y ) -> j e. X ) |
53 |
51 52
|
ffvelrnd |
|- ( ( ph /\ j e. Y ) -> ( G ` j ) e. S ) |
54 |
50 53
|
ffvelrnd |
|- ( ( ph /\ j e. Y ) -> ( M ` ( G ` j ) ) e. ( 0 [,] +oo ) ) |
55 |
|
eldifi |
|- ( j e. ( X \ Y ) -> j e. X ) |
56 |
55
|
ad2antlr |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> j e. X ) |
57 |
|
fveq2 |
|- ( ( G ` j ) = (/) -> ( M ` ( G ` j ) ) = ( M ` (/) ) ) |
58 |
57
|
adantl |
|- ( ( ph /\ ( G ` j ) = (/) ) -> ( M ` ( G ` j ) ) = ( M ` (/) ) ) |
59 |
1
|
adantr |
|- ( ( ph /\ ( G ` j ) = (/) ) -> M e. Meas ) |
60 |
59
|
mea0 |
|- ( ( ph /\ ( G ` j ) = (/) ) -> ( M ` (/) ) = 0 ) |
61 |
58 60
|
eqtrd |
|- ( ( ph /\ ( G ` j ) = (/) ) -> ( M ` ( G ` j ) ) = 0 ) |
62 |
61
|
ad4ant14 |
|- ( ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) /\ ( G ` j ) = (/) ) -> ( M ` ( G ` j ) ) = 0 ) |
63 |
|
neneq |
|- ( ( M ` ( G ` j ) ) =/= 0 -> -. ( M ` ( G ` j ) ) = 0 ) |
64 |
63
|
ad2antlr |
|- ( ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) /\ ( G ` j ) = (/) ) -> -. ( M ` ( G ` j ) ) = 0 ) |
65 |
62 64
|
pm2.65da |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> -. ( G ` j ) = (/) ) |
66 |
65
|
neqned |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> ( G ` j ) =/= (/) ) |
67 |
56 66
|
jca |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> ( j e. X /\ ( G ` j ) =/= (/) ) ) |
68 |
|
fveq2 |
|- ( i = j -> ( G ` i ) = ( G ` j ) ) |
69 |
68
|
neeq1d |
|- ( i = j -> ( ( G ` i ) =/= (/) <-> ( G ` j ) =/= (/) ) ) |
70 |
69
|
elrab |
|- ( j e. { i e. X | ( G ` i ) =/= (/) } <-> ( j e. X /\ ( G ` j ) =/= (/) ) ) |
71 |
67 70
|
sylibr |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> j e. { i e. X | ( G ` i ) =/= (/) } ) |
72 |
71 5
|
eleqtrrdi |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> j e. Y ) |
73 |
|
eldifn |
|- ( j e. ( X \ Y ) -> -. j e. Y ) |
74 |
73
|
ad2antlr |
|- ( ( ( ph /\ j e. ( X \ Y ) ) /\ ( M ` ( G ` j ) ) =/= 0 ) -> -. j e. Y ) |
75 |
72 74
|
pm2.65da |
|- ( ( ph /\ j e. ( X \ Y ) ) -> -. ( M ` ( G ` j ) ) =/= 0 ) |
76 |
|
nne |
|- ( -. ( M ` ( G ` j ) ) =/= 0 <-> ( M ` ( G ` j ) ) = 0 ) |
77 |
75 76
|
sylib |
|- ( ( ph /\ j e. ( X \ Y ) ) -> ( M ` ( G ` j ) ) = 0 ) |
78 |
46 3 49 54 77
|
sge0ss |
|- ( ph -> ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) = ( sum^ ` ( j e. X |-> ( M ` ( G ` j ) ) ) ) ) |
79 |
78
|
eqcomd |
|- ( ph -> ( sum^ ` ( j e. X |-> ( M ` ( G ` j ) ) ) ) = ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) ) |
80 |
3 49
|
ssexd |
|- ( ph -> Y e. _V ) |
81 |
|
nfv |
|- F/ i ph |
82 |
|
eqid |
|- ( i e. Y |-> ( G ` i ) ) = ( i e. Y |-> ( G ` i ) ) |
83 |
4
|
ffnd |
|- ( ph -> G Fn X ) |
84 |
|
dffn3 |
|- ( G Fn X <-> G : X --> ran G ) |
85 |
83 84
|
sylib |
|- ( ph -> G : X --> ran G ) |
86 |
85
|
adantr |
|- ( ( ph /\ i e. Y ) -> G : X --> ran G ) |
87 |
49
|
sselda |
|- ( ( ph /\ i e. Y ) -> i e. X ) |
88 |
86 87
|
ffvelrnd |
|- ( ( ph /\ i e. Y ) -> ( G ` i ) e. ran G ) |
89 |
5
|
eleq2i |
|- ( i e. Y <-> i e. { i e. X | ( G ` i ) =/= (/) } ) |
90 |
|
rabid |
|- ( i e. { i e. X | ( G ` i ) =/= (/) } <-> ( i e. X /\ ( G ` i ) =/= (/) ) ) |
91 |
89 90
|
bitri |
|- ( i e. Y <-> ( i e. X /\ ( G ` i ) =/= (/) ) ) |
92 |
91
|
biimpi |
|- ( i e. Y -> ( i e. X /\ ( G ` i ) =/= (/) ) ) |
93 |
92
|
simprd |
|- ( i e. Y -> ( G ` i ) =/= (/) ) |
94 |
93
|
adantl |
|- ( ( ph /\ i e. Y ) -> ( G ` i ) =/= (/) ) |
95 |
|
nelsn |
|- ( ( G ` i ) =/= (/) -> -. ( G ` i ) e. { (/) } ) |
96 |
94 95
|
syl |
|- ( ( ph /\ i e. Y ) -> -. ( G ` i ) e. { (/) } ) |
97 |
88 96
|
eldifd |
|- ( ( ph /\ i e. Y ) -> ( G ` i ) e. ( ran G \ { (/) } ) ) |
98 |
|
disjss1 |
|- ( Y C_ X -> ( Disj_ i e. X ( G ` i ) -> Disj_ i e. Y ( G ` i ) ) ) |
99 |
49 6 98
|
sylc |
|- ( ph -> Disj_ i e. Y ( G ` i ) ) |
100 |
81 82 97 94 99
|
disjf1 |
|- ( ph -> ( i e. Y |-> ( G ` i ) ) : Y -1-1-> ( ran G \ { (/) } ) ) |
101 |
4 49
|
feqresmpt |
|- ( ph -> ( G |` Y ) = ( i e. Y |-> ( G ` i ) ) ) |
102 |
|
f1eq1 |
|- ( ( G |` Y ) = ( i e. Y |-> ( G ` i ) ) -> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) <-> ( i e. Y |-> ( G ` i ) ) : Y -1-1-> ( ran G \ { (/) } ) ) ) |
103 |
101 102
|
syl |
|- ( ph -> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) <-> ( i e. Y |-> ( G ` i ) ) : Y -1-1-> ( ran G \ { (/) } ) ) ) |
104 |
100 103
|
mpbird |
|- ( ph -> ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) ) |
105 |
101
|
rneqd |
|- ( ph -> ran ( G |` Y ) = ran ( i e. Y |-> ( G ` i ) ) ) |
106 |
97
|
ralrimiva |
|- ( ph -> A. i e. Y ( G ` i ) e. ( ran G \ { (/) } ) ) |
107 |
82
|
rnmptss |
|- ( A. i e. Y ( G ` i ) e. ( ran G \ { (/) } ) -> ran ( i e. Y |-> ( G ` i ) ) C_ ( ran G \ { (/) } ) ) |
108 |
106 107
|
syl |
|- ( ph -> ran ( i e. Y |-> ( G ` i ) ) C_ ( ran G \ { (/) } ) ) |
109 |
105 108
|
eqsstrd |
|- ( ph -> ran ( G |` Y ) C_ ( ran G \ { (/) } ) ) |
110 |
|
simpl |
|- ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> ph ) |
111 |
|
eldifi |
|- ( x e. ( ran G \ { (/) } ) -> x e. ran G ) |
112 |
111
|
adantl |
|- ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> x e. ran G ) |
113 |
|
eldifsni |
|- ( x e. ( ran G \ { (/) } ) -> x =/= (/) ) |
114 |
113
|
adantl |
|- ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> x =/= (/) ) |
115 |
|
simpr |
|- ( ( ph /\ x e. ran G ) -> x e. ran G ) |
116 |
|
fvelrnb |
|- ( G Fn X -> ( x e. ran G <-> E. i e. X ( G ` i ) = x ) ) |
117 |
83 116
|
syl |
|- ( ph -> ( x e. ran G <-> E. i e. X ( G ` i ) = x ) ) |
118 |
117
|
adantr |
|- ( ( ph /\ x e. ran G ) -> ( x e. ran G <-> E. i e. X ( G ` i ) = x ) ) |
119 |
115 118
|
mpbid |
|- ( ( ph /\ x e. ran G ) -> E. i e. X ( G ` i ) = x ) |
120 |
119
|
3adant3 |
|- ( ( ph /\ x e. ran G /\ x =/= (/) ) -> E. i e. X ( G ` i ) = x ) |
121 |
|
id |
|- ( ( G ` i ) = x -> ( G ` i ) = x ) |
122 |
121
|
eqcomd |
|- ( ( G ` i ) = x -> x = ( G ` i ) ) |
123 |
122
|
3ad2ant3 |
|- ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> x = ( G ` i ) ) |
124 |
|
simp1l |
|- ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> ph ) |
125 |
|
simp2 |
|- ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> i e. X ) |
126 |
|
simpr |
|- ( ( x =/= (/) /\ ( G ` i ) = x ) -> ( G ` i ) = x ) |
127 |
|
simpl |
|- ( ( x =/= (/) /\ ( G ` i ) = x ) -> x =/= (/) ) |
128 |
126 127
|
eqnetrd |
|- ( ( x =/= (/) /\ ( G ` i ) = x ) -> ( G ` i ) =/= (/) ) |
129 |
128
|
adantll |
|- ( ( ( ph /\ x =/= (/) ) /\ ( G ` i ) = x ) -> ( G ` i ) =/= (/) ) |
130 |
129
|
3adant2 |
|- ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> ( G ` i ) =/= (/) ) |
131 |
91
|
biimpri |
|- ( ( i e. X /\ ( G ` i ) =/= (/) ) -> i e. Y ) |
132 |
|
fvexd |
|- ( ( i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. _V ) |
133 |
82
|
elrnmpt1 |
|- ( ( i e. Y /\ ( G ` i ) e. _V ) -> ( G ` i ) e. ran ( i e. Y |-> ( G ` i ) ) ) |
134 |
131 132 133
|
syl2anc |
|- ( ( i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. ran ( i e. Y |-> ( G ` i ) ) ) |
135 |
134
|
3adant1 |
|- ( ( ph /\ i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. ran ( i e. Y |-> ( G ` i ) ) ) |
136 |
105
|
eqcomd |
|- ( ph -> ran ( i e. Y |-> ( G ` i ) ) = ran ( G |` Y ) ) |
137 |
136
|
3ad2ant1 |
|- ( ( ph /\ i e. X /\ ( G ` i ) =/= (/) ) -> ran ( i e. Y |-> ( G ` i ) ) = ran ( G |` Y ) ) |
138 |
135 137
|
eleqtrd |
|- ( ( ph /\ i e. X /\ ( G ` i ) =/= (/) ) -> ( G ` i ) e. ran ( G |` Y ) ) |
139 |
124 125 130 138
|
syl3anc |
|- ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> ( G ` i ) e. ran ( G |` Y ) ) |
140 |
123 139
|
eqeltrd |
|- ( ( ( ph /\ x =/= (/) ) /\ i e. X /\ ( G ` i ) = x ) -> x e. ran ( G |` Y ) ) |
141 |
140
|
3exp |
|- ( ( ph /\ x =/= (/) ) -> ( i e. X -> ( ( G ` i ) = x -> x e. ran ( G |` Y ) ) ) ) |
142 |
141
|
rexlimdv |
|- ( ( ph /\ x =/= (/) ) -> ( E. i e. X ( G ` i ) = x -> x e. ran ( G |` Y ) ) ) |
143 |
142
|
3adant2 |
|- ( ( ph /\ x e. ran G /\ x =/= (/) ) -> ( E. i e. X ( G ` i ) = x -> x e. ran ( G |` Y ) ) ) |
144 |
120 143
|
mpd |
|- ( ( ph /\ x e. ran G /\ x =/= (/) ) -> x e. ran ( G |` Y ) ) |
145 |
110 112 114 144
|
syl3anc |
|- ( ( ph /\ x e. ( ran G \ { (/) } ) ) -> x e. ran ( G |` Y ) ) |
146 |
109 145
|
eqelssd |
|- ( ph -> ran ( G |` Y ) = ( ran G \ { (/) } ) ) |
147 |
104 146
|
jca |
|- ( ph -> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) /\ ran ( G |` Y ) = ( ran G \ { (/) } ) ) ) |
148 |
|
dff1o5 |
|- ( ( G |` Y ) : Y -1-1-onto-> ( ran G \ { (/) } ) <-> ( ( G |` Y ) : Y -1-1-> ( ran G \ { (/) } ) /\ ran ( G |` Y ) = ( ran G \ { (/) } ) ) ) |
149 |
147 148
|
sylibr |
|- ( ph -> ( G |` Y ) : Y -1-1-onto-> ( ran G \ { (/) } ) ) |
150 |
|
fvres |
|- ( j e. Y -> ( ( G |` Y ) ` j ) = ( G ` j ) ) |
151 |
150
|
adantl |
|- ( ( ph /\ j e. Y ) -> ( ( G |` Y ) ` j ) = ( G ` j ) ) |
152 |
7 46 43 80 149 151 19
|
sge0f1o |
|- ( ph -> ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) = ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) ) |
153 |
152
|
eqcomd |
|- ( ph -> ( sum^ ` ( j e. Y |-> ( M ` ( G ` j ) ) ) ) = ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) ) |
154 |
45 79 153
|
3eqtrd |
|- ( ph -> ( sum^ ` ( M o. G ) ) = ( sum^ ` ( k e. ( ran G \ { (/) } ) |-> ( M ` k ) ) ) ) |
155 |
37 39 154
|
3eqtr4d |
|- ( ph -> ( sum^ ` ( M |` ran G ) ) = ( sum^ ` ( M o. G ) ) ) |