Step |
Hyp |
Ref |
Expression |
1 |
|
sge0xp.1 |
|- F/ k ph |
2 |
|
sge0xp.z |
|- ( z = <. j , k >. -> D = C ) |
3 |
|
sge0xp.a |
|- ( ph -> A e. V ) |
4 |
|
sge0xp.b |
|- ( ph -> B e. W ) |
5 |
|
sge0xp.d |
|- ( ( ph /\ j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) ) |
6 |
|
snex |
|- { j } e. _V |
7 |
6
|
a1i |
|- ( ph -> { j } e. _V ) |
8 |
7 4
|
xpexd |
|- ( ph -> ( { j } X. B ) e. _V ) |
9 |
8
|
adantr |
|- ( ( ph /\ j e. A ) -> ( { j } X. B ) e. _V ) |
10 |
|
disjsnxp |
|- Disj_ j e. A ( { j } X. B ) |
11 |
10
|
a1i |
|- ( ph -> Disj_ j e. A ( { j } X. B ) ) |
12 |
|
vex |
|- j e. _V |
13 |
|
elsnxp |
|- ( j e. _V -> ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) ) |
14 |
12 13
|
ax-mp |
|- ( z e. ( { j } X. B ) <-> E. k e. B z = <. j , k >. ) |
15 |
14
|
biimpi |
|- ( z e. ( { j } X. B ) -> E. k e. B z = <. j , k >. ) |
16 |
15
|
adantl |
|- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> E. k e. B z = <. j , k >. ) |
17 |
|
nfv |
|- F/ k j e. A |
18 |
1 17
|
nfan |
|- F/ k ( ph /\ j e. A ) |
19 |
|
nfv |
|- F/ k z e. ( { j } X. B ) |
20 |
18 19
|
nfan |
|- F/ k ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) |
21 |
|
nfv |
|- F/ k D e. ( 0 [,] +oo ) |
22 |
2
|
3ad2ant3 |
|- ( ( ( ph /\ j e. A ) /\ k e. B /\ z = <. j , k >. ) -> D = C ) |
23 |
5
|
3expa |
|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. ( 0 [,] +oo ) ) |
24 |
23
|
3adant3 |
|- ( ( ( ph /\ j e. A ) /\ k e. B /\ z = <. j , k >. ) -> C e. ( 0 [,] +oo ) ) |
25 |
22 24
|
eqeltrd |
|- ( ( ( ph /\ j e. A ) /\ k e. B /\ z = <. j , k >. ) -> D e. ( 0 [,] +oo ) ) |
26 |
25
|
3exp |
|- ( ( ph /\ j e. A ) -> ( k e. B -> ( z = <. j , k >. -> D e. ( 0 [,] +oo ) ) ) ) |
27 |
26
|
adantr |
|- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( k e. B -> ( z = <. j , k >. -> D e. ( 0 [,] +oo ) ) ) ) |
28 |
20 21 27
|
rexlimd |
|- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> ( E. k e. B z = <. j , k >. -> D e. ( 0 [,] +oo ) ) ) |
29 |
16 28
|
mpd |
|- ( ( ( ph /\ j e. A ) /\ z e. ( { j } X. B ) ) -> D e. ( 0 [,] +oo ) ) |
30 |
29
|
3impa |
|- ( ( ph /\ j e. A /\ z e. ( { j } X. B ) ) -> D e. ( 0 [,] +oo ) ) |
31 |
3 9 11 30
|
sge0iunmpt |
|- ( ph -> ( sum^ ` ( z e. U_ j e. A ( { j } X. B ) |-> D ) ) = ( sum^ ` ( j e. A |-> ( sum^ ` ( z e. ( { j } X. B ) |-> D ) ) ) ) ) |
32 |
|
iunxpconst |
|- U_ j e. A ( { j } X. B ) = ( A X. B ) |
33 |
32
|
eqcomi |
|- ( A X. B ) = U_ j e. A ( { j } X. B ) |
34 |
33
|
a1i |
|- ( ph -> ( A X. B ) = U_ j e. A ( { j } X. B ) ) |
35 |
34
|
mpteq1d |
|- ( ph -> ( z e. ( A X. B ) |-> D ) = ( z e. U_ j e. A ( { j } X. B ) |-> D ) ) |
36 |
35
|
fveq2d |
|- ( ph -> ( sum^ ` ( z e. ( A X. B ) |-> D ) ) = ( sum^ ` ( z e. U_ j e. A ( { j } X. B ) |-> D ) ) ) |
37 |
|
nfv |
|- F/ j ph |
38 |
|
nfv |
|- F/ z ( ph /\ j e. A ) |
39 |
4
|
adantr |
|- ( ( ph /\ j e. A ) -> B e. W ) |
40 |
|
simpr |
|- ( ( ph /\ j e. A ) -> j e. A ) |
41 |
|
eqid |
|- ( i e. B |-> <. j , i >. ) = ( i e. B |-> <. j , i >. ) |
42 |
40 41
|
projf1o |
|- ( ( ph /\ j e. A ) -> ( i e. B |-> <. j , i >. ) : B -1-1-onto-> ( { j } X. B ) ) |
43 |
|
eqidd |
|- ( ( ph /\ k e. B ) -> ( i e. B |-> <. j , i >. ) = ( i e. B |-> <. j , i >. ) ) |
44 |
|
opeq2 |
|- ( i = k -> <. j , i >. = <. j , k >. ) |
45 |
44
|
adantl |
|- ( ( ( ph /\ k e. B ) /\ i = k ) -> <. j , i >. = <. j , k >. ) |
46 |
|
simpr |
|- ( ( ph /\ k e. B ) -> k e. B ) |
47 |
|
opex |
|- <. j , k >. e. _V |
48 |
47
|
a1i |
|- ( ( ph /\ k e. B ) -> <. j , k >. e. _V ) |
49 |
43 45 46 48
|
fvmptd |
|- ( ( ph /\ k e. B ) -> ( ( i e. B |-> <. j , i >. ) ` k ) = <. j , k >. ) |
50 |
49
|
adantlr |
|- ( ( ( ph /\ j e. A ) /\ k e. B ) -> ( ( i e. B |-> <. j , i >. ) ` k ) = <. j , k >. ) |
51 |
38 18 2 39 42 50 29
|
sge0f1o |
|- ( ( ph /\ j e. A ) -> ( sum^ ` ( z e. ( { j } X. B ) |-> D ) ) = ( sum^ ` ( k e. B |-> C ) ) ) |
52 |
51
|
eqcomd |
|- ( ( ph /\ j e. A ) -> ( sum^ ` ( k e. B |-> C ) ) = ( sum^ ` ( z e. ( { j } X. B ) |-> D ) ) ) |
53 |
37 52
|
mpteq2da |
|- ( ph -> ( j e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) = ( j e. A |-> ( sum^ ` ( z e. ( { j } X. B ) |-> D ) ) ) ) |
54 |
53
|
fveq2d |
|- ( ph -> ( sum^ ` ( j e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( j e. A |-> ( sum^ ` ( z e. ( { j } X. B ) |-> D ) ) ) ) ) |
55 |
31 36 54
|
3eqtr4rd |
|- ( ph -> ( sum^ ` ( j e. A |-> ( sum^ ` ( k e. B |-> C ) ) ) ) = ( sum^ ` ( z e. ( A X. B ) |-> D ) ) ) |