Step |
Hyp |
Ref |
Expression |
1 |
|
esumiun.0 |
|- ( ph -> A e. V ) |
2 |
|
esumiun.1 |
|- ( ( ph /\ j e. A ) -> B e. W ) |
3 |
|
esumiun.2 |
|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) ) |
4 |
1 2
|
aciunf1 |
|- ( ph -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) ) |
5 |
|
f1f1orn |
|- ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) -> f : U_ j e. A B -1-1-onto-> ran f ) |
6 |
5
|
anim1i |
|- ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) ) |
7 |
|
f1f |
|- ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) -> f : U_ j e. A B --> U_ j e. A ( { j } X. B ) ) |
8 |
7
|
frnd |
|- ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) -> ran f C_ U_ j e. A ( { j } X. B ) ) |
9 |
8
|
adantr |
|- ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ran f C_ U_ j e. A ( { j } X. B ) ) |
10 |
6 9
|
jca |
|- ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) |
11 |
10
|
eximi |
|- ( E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> E. f ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) |
12 |
4 11
|
syl |
|- ( ph -> E. f ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) |
13 |
|
nfv |
|- F/ z ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) |
14 |
|
nfcv |
|- F/_ z C |
15 |
|
nfcsb1v |
|- F/_ k [_ ( 2nd ` z ) / k ]_ C |
16 |
|
nfcv |
|- F/_ z U_ j e. A B |
17 |
|
nfcv |
|- F/_ z ran f |
18 |
|
nfcv |
|- F/_ z `' f |
19 |
|
csbeq1a |
|- ( k = ( 2nd ` z ) -> C = [_ ( 2nd ` z ) / k ]_ C ) |
20 |
2
|
ralrimiva |
|- ( ph -> A. j e. A B e. W ) |
21 |
|
iunexg |
|- ( ( A e. V /\ A. j e. A B e. W ) -> U_ j e. A B e. _V ) |
22 |
1 20 21
|
syl2anc |
|- ( ph -> U_ j e. A B e. _V ) |
23 |
22
|
adantr |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> U_ j e. A B e. _V ) |
24 |
|
simprl |
|- ( ( ph /\ ( f : U_ j e. A B -1-1-onto-> ran f /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> f : U_ j e. A B -1-1-onto-> ran f ) |
25 |
|
f1ocnv |
|- ( f : U_ j e. A B -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> U_ j e. A B ) |
26 |
24 25
|
syl |
|- ( ( ph /\ ( f : U_ j e. A B -1-1-onto-> ran f /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ j e. A B ) |
27 |
26
|
adantrlr |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ j e. A B ) |
28 |
|
nfv |
|- F/ j ph |
29 |
|
nfcv |
|- F/_ j f |
30 |
|
nfiu1 |
|- F/_ j U_ j e. A B |
31 |
29
|
nfrn |
|- F/_ j ran f |
32 |
29 30 31
|
nff1o |
|- F/ j f : U_ j e. A B -1-1-onto-> ran f |
33 |
|
nfv |
|- F/ j ( 2nd ` ( f ` l ) ) = l |
34 |
30 33
|
nfralw |
|- F/ j A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l |
35 |
32 34
|
nfan |
|- F/ j ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) |
36 |
|
nfcv |
|- F/_ j ran f |
37 |
|
nfiu1 |
|- F/_ j U_ j e. A ( { j } X. B ) |
38 |
36 37
|
nfss |
|- F/ j ran f C_ U_ j e. A ( { j } X. B ) |
39 |
35 38
|
nfan |
|- F/ j ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) |
40 |
28 39
|
nfan |
|- F/ j ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) |
41 |
|
nfv |
|- F/ j z e. ran f |
42 |
40 41
|
nfan |
|- F/ j ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) |
43 |
|
simpr |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( f ` k ) = z ) |
44 |
43
|
fveq2d |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = ( 2nd ` z ) ) |
45 |
|
simplr |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> k e. U_ j e. A B ) |
46 |
|
simp-4r |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) |
47 |
46
|
simpld |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) ) |
48 |
47
|
simprd |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) |
49 |
48
|
ad2antrr |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) |
50 |
|
2fveq3 |
|- ( l = k -> ( 2nd ` ( f ` l ) ) = ( 2nd ` ( f ` k ) ) ) |
51 |
|
id |
|- ( l = k -> l = k ) |
52 |
50 51
|
eqeq12d |
|- ( l = k -> ( ( 2nd ` ( f ` l ) ) = l <-> ( 2nd ` ( f ` k ) ) = k ) ) |
53 |
52
|
rspcva |
|- ( ( k e. U_ j e. A B /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( 2nd ` ( f ` k ) ) = k ) |
54 |
45 49 53
|
syl2anc |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = k ) |
55 |
44 54
|
eqtr3d |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` z ) = k ) |
56 |
47
|
simpld |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> f : U_ j e. A B -1-1-onto-> ran f ) |
57 |
56
|
ad2antrr |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> f : U_ j e. A B -1-1-onto-> ran f ) |
58 |
|
f1ocnvfv1 |
|- ( ( f : U_ j e. A B -1-1-onto-> ran f /\ k e. U_ j e. A B ) -> ( `' f ` ( f ` k ) ) = k ) |
59 |
57 45 58
|
syl2anc |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = k ) |
60 |
43
|
fveq2d |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = ( `' f ` z ) ) |
61 |
55 59 60
|
3eqtr2rd |
|- ( ( ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) /\ k e. U_ j e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` z ) = ( 2nd ` z ) ) |
62 |
|
f1ofn |
|- ( f : U_ j e. A B -1-1-onto-> ran f -> f Fn U_ j e. A B ) |
63 |
56 62
|
syl |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> f Fn U_ j e. A B ) |
64 |
|
simpllr |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> z e. ran f ) |
65 |
|
fvelrnb |
|- ( f Fn U_ j e. A B -> ( z e. ran f <-> E. k e. U_ j e. A B ( f ` k ) = z ) ) |
66 |
65
|
biimpa |
|- ( ( f Fn U_ j e. A B /\ z e. ran f ) -> E. k e. U_ j e. A B ( f ` k ) = z ) |
67 |
63 64 66
|
syl2anc |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E. k e. U_ j e. A B ( f ` k ) = z ) |
68 |
61 67
|
r19.29a |
|- ( ( ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( `' f ` z ) = ( 2nd ` z ) ) |
69 |
|
simprr |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> ran f C_ U_ j e. A ( { j } X. B ) ) |
70 |
69
|
sselda |
|- ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) -> z e. U_ j e. A ( { j } X. B ) ) |
71 |
|
eliun |
|- ( z e. U_ j e. A ( { j } X. B ) <-> E. j e. A z e. ( { j } X. B ) ) |
72 |
70 71
|
sylib |
|- ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) -> E. j e. A z e. ( { j } X. B ) ) |
73 |
42 68 72
|
r19.29af |
|- ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. ran f ) -> ( `' f ` z ) = ( 2nd ` z ) ) |
74 |
|
nfcv |
|- F/_ j k |
75 |
74 30
|
nfel |
|- F/ j k e. U_ j e. A B |
76 |
28 75
|
nfan |
|- F/ j ( ph /\ k e. U_ j e. A B ) |
77 |
3
|
adantllr |
|- ( ( ( ( ph /\ k e. U_ j e. A B ) /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) ) |
78 |
|
eliun |
|- ( k e. U_ j e. A B <-> E. j e. A k e. B ) |
79 |
78
|
biimpi |
|- ( k e. U_ j e. A B -> E. j e. A k e. B ) |
80 |
79
|
adantl |
|- ( ( ph /\ k e. U_ j e. A B ) -> E. j e. A k e. B ) |
81 |
76 77 80
|
r19.29af |
|- ( ( ph /\ k e. U_ j e. A B ) -> C e. ( 0 [,] +oo ) ) |
82 |
81
|
adantlr |
|- ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ k e. U_ j e. A B ) -> C e. ( 0 [,] +oo ) ) |
83 |
13 14 15 16 17 18 19 23 27 73 82
|
esumf1o |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* k e. U_ j e. A B C = sum* z e. ran f [_ ( 2nd ` z ) / k ]_ C ) |
84 |
83
|
eqcomd |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* z e. ran f [_ ( 2nd ` z ) / k ]_ C = sum* k e. U_ j e. A B C ) |
85 |
|
snex |
|- { j } e. _V |
86 |
85
|
a1i |
|- ( ( ph /\ j e. A ) -> { j } e. _V ) |
87 |
86 2
|
xpexd |
|- ( ( ph /\ j e. A ) -> ( { j } X. B ) e. _V ) |
88 |
87
|
ralrimiva |
|- ( ph -> A. j e. A ( { j } X. B ) e. _V ) |
89 |
|
iunexg |
|- ( ( A e. V /\ A. j e. A ( { j } X. B ) e. _V ) -> U_ j e. A ( { j } X. B ) e. _V ) |
90 |
1 88 89
|
syl2anc |
|- ( ph -> U_ j e. A ( { j } X. B ) e. _V ) |
91 |
90
|
adantr |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> U_ j e. A ( { j } X. B ) e. _V ) |
92 |
|
nfcv |
|- F/_ j z |
93 |
92 37
|
nfel |
|- F/ j z e. U_ j e. A ( { j } X. B ) |
94 |
28 93
|
nfan |
|- F/ j ( ph /\ z e. U_ j e. A ( { j } X. B ) ) |
95 |
|
nfcv |
|- F/_ j ( 2nd ` z ) |
96 |
|
nfcv |
|- F/_ j C |
97 |
95 96
|
nfcsbw |
|- F/_ j [_ ( 2nd ` z ) / k ]_ C |
98 |
|
nfcv |
|- F/_ j ( 0 [,] +oo ) |
99 |
97 98
|
nfel |
|- F/ j [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) |
100 |
|
simprr |
|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> ( 2nd ` z ) e. B ) |
101 |
|
simplll |
|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> ph ) |
102 |
|
simplr |
|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> j e. A ) |
103 |
3
|
ralrimiva |
|- ( ( ph /\ j e. A ) -> A. k e. B C e. ( 0 [,] +oo ) ) |
104 |
101 102 103
|
syl2anc |
|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> A. k e. B C e. ( 0 [,] +oo ) ) |
105 |
|
rspcsbela |
|- ( ( ( 2nd ` z ) e. B /\ A. k e. B C e. ( 0 [,] +oo ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) ) |
106 |
100 104 105
|
syl2anc |
|- ( ( ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) /\ j e. A ) /\ ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) ) |
107 |
|
xp1st |
|- ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } ) |
108 |
|
elsni |
|- ( ( 1st ` z ) e. { j } -> ( 1st ` z ) = j ) |
109 |
107 108
|
syl |
|- ( z e. ( { j } X. B ) -> ( 1st ` z ) = j ) |
110 |
|
xp2nd |
|- ( z e. ( { j } X. B ) -> ( 2nd ` z ) e. B ) |
111 |
109 110
|
jca |
|- ( z e. ( { j } X. B ) -> ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) |
112 |
111
|
reximi |
|- ( E. j e. A z e. ( { j } X. B ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) |
113 |
71 112
|
sylbi |
|- ( z e. U_ j e. A ( { j } X. B ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) |
114 |
113
|
adantl |
|- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> E. j e. A ( ( 1st ` z ) = j /\ ( 2nd ` z ) e. B ) ) |
115 |
94 99 106 114
|
r19.29af2 |
|- ( ( ph /\ z e. U_ j e. A ( { j } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) ) |
116 |
115
|
adantlr |
|- ( ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) /\ z e. U_ j e. A ( { j } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. ( 0 [,] +oo ) ) |
117 |
|
simprr |
|- ( ( ph /\ ( f : U_ j e. A B -1-1-onto-> ran f /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> ran f C_ U_ j e. A ( { j } X. B ) ) |
118 |
117
|
adantrlr |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> ran f C_ U_ j e. A ( { j } X. B ) ) |
119 |
13 91 116 118
|
esummono |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* z e. ran f [_ ( 2nd ` z ) / k ]_ C <_ sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C ) |
120 |
84 119
|
eqbrtrrd |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* k e. U_ j e. A B C <_ sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C ) |
121 |
|
vex |
|- j e. _V |
122 |
|
vex |
|- k e. _V |
123 |
121 122
|
op2ndd |
|- ( z = <. j , k >. -> ( 2nd ` z ) = k ) |
124 |
123
|
eqcomd |
|- ( z = <. j , k >. -> k = ( 2nd ` z ) ) |
125 |
124 19
|
syl |
|- ( z = <. j , k >. -> C = [_ ( 2nd ` z ) / k ]_ C ) |
126 |
125
|
eqcomd |
|- ( z = <. j , k >. -> [_ ( 2nd ` z ) / k ]_ C = C ) |
127 |
3
|
anasss |
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. ( 0 [,] +oo ) ) |
128 |
15 126 1 2 127
|
esum2d |
|- ( ph -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C ) |
129 |
128
|
adantr |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* j e. A sum* k e. B C = sum* z e. U_ j e. A ( { j } X. B ) [_ ( 2nd ` z ) / k ]_ C ) |
130 |
120 129
|
breqtrrd |
|- ( ( ph /\ ( ( f : U_ j e. A B -1-1-onto-> ran f /\ A. l e. U_ j e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ j e. A ( { j } X. B ) ) ) -> sum* k e. U_ j e. A B C <_ sum* j e. A sum* k e. B C ) |
131 |
12 130
|
exlimddv |
|- ( ph -> sum* k e. U_ j e. A B C <_ sum* j e. A sum* k e. B C ) |