Step |
Hyp |
Ref |
Expression |
1 |
|
gsum2d2.b |
|- B = ( Base ` G ) |
2 |
|
gsum2d2.z |
|- .0. = ( 0g ` G ) |
3 |
|
gsum2d2.g |
|- ( ph -> G e. CMnd ) |
4 |
|
gsum2d2.a |
|- ( ph -> A e. V ) |
5 |
|
gsum2d2.r |
|- ( ( ph /\ j e. A ) -> C e. W ) |
6 |
|
gsum2d2.f |
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B ) |
7 |
|
gsum2d2.u |
|- ( ph -> U e. Fin ) |
8 |
|
gsum2d2.n |
|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. ) |
9 |
|
snex |
|- { j } e. _V |
10 |
|
xpexg |
|- ( ( { j } e. _V /\ C e. W ) -> ( { j } X. C ) e. _V ) |
11 |
9 5 10
|
sylancr |
|- ( ( ph /\ j e. A ) -> ( { j } X. C ) e. _V ) |
12 |
11
|
ralrimiva |
|- ( ph -> A. j e. A ( { j } X. C ) e. _V ) |
13 |
|
iunexg |
|- ( ( A e. V /\ A. j e. A ( { j } X. C ) e. _V ) -> U_ j e. A ( { j } X. C ) e. _V ) |
14 |
4 12 13
|
syl2anc |
|- ( ph -> U_ j e. A ( { j } X. C ) e. _V ) |
15 |
|
relxp |
|- Rel ( { j } X. C ) |
16 |
15
|
rgenw |
|- A. j e. A Rel ( { j } X. C ) |
17 |
|
reliun |
|- ( Rel U_ j e. A ( { j } X. C ) <-> A. j e. A Rel ( { j } X. C ) ) |
18 |
16 17
|
mpbir |
|- Rel U_ j e. A ( { j } X. C ) |
19 |
18
|
a1i |
|- ( ph -> Rel U_ j e. A ( { j } X. C ) ) |
20 |
|
vex |
|- x e. _V |
21 |
20
|
eldm2 |
|- ( x e. dom U_ j e. A ( { j } X. C ) <-> E. y <. x , y >. e. U_ j e. A ( { j } X. C ) ) |
22 |
|
eliunxp |
|- ( <. x , y >. e. U_ j e. A ( { j } X. C ) <-> E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) |
23 |
|
vex |
|- y e. _V |
24 |
20 23
|
opth1 |
|- ( <. x , y >. = <. j , k >. -> x = j ) |
25 |
24
|
ad2antrl |
|- ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> x = j ) |
26 |
|
simprrl |
|- ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> j e. A ) |
27 |
25 26
|
eqeltrd |
|- ( ( ph /\ ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) ) -> x e. A ) |
28 |
27
|
ex |
|- ( ph -> ( ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) -> x e. A ) ) |
29 |
28
|
exlimdvv |
|- ( ph -> ( E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. C ) ) -> x e. A ) ) |
30 |
22 29
|
syl5bi |
|- ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. C ) -> x e. A ) ) |
31 |
30
|
exlimdv |
|- ( ph -> ( E. y <. x , y >. e. U_ j e. A ( { j } X. C ) -> x e. A ) ) |
32 |
21 31
|
syl5bi |
|- ( ph -> ( x e. dom U_ j e. A ( { j } X. C ) -> x e. A ) ) |
33 |
32
|
ssrdv |
|- ( ph -> dom U_ j e. A ( { j } X. C ) C_ A ) |
34 |
6
|
ralrimivva |
|- ( ph -> A. j e. A A. k e. C X e. B ) |
35 |
|
eqid |
|- ( j e. A , k e. C |-> X ) = ( j e. A , k e. C |-> X ) |
36 |
35
|
fmpox |
|- ( A. j e. A A. k e. C X e. B <-> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B ) |
37 |
34 36
|
sylib |
|- ( ph -> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B ) |
38 |
1 2 3 4 5 6 7 8
|
gsum2d2lem |
|- ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. ) |
39 |
1 2 3 14 19 4 33 37 38
|
gsum2d |
|- ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) ) ) |
40 |
|
nfcv |
|- F/_ j G |
41 |
|
nfcv |
|- F/_ j gsum |
42 |
|
nfiu1 |
|- F/_ j U_ j e. A ( { j } X. C ) |
43 |
|
nfcv |
|- F/_ j { m } |
44 |
42 43
|
nfima |
|- F/_ j ( U_ j e. A ( { j } X. C ) " { m } ) |
45 |
|
nfcv |
|- F/_ j m |
46 |
|
nfmpo1 |
|- F/_ j ( j e. A , k e. C |-> X ) |
47 |
|
nfcv |
|- F/_ j n |
48 |
45 46 47
|
nfov |
|- F/_ j ( m ( j e. A , k e. C |-> X ) n ) |
49 |
44 48
|
nfmpt |
|- F/_ j ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) |
50 |
40 41 49
|
nfov |
|- F/_ j ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) |
51 |
|
nfcv |
|- F/_ m ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) |
52 |
|
sneq |
|- ( m = j -> { m } = { j } ) |
53 |
52
|
imaeq2d |
|- ( m = j -> ( U_ j e. A ( { j } X. C ) " { m } ) = ( U_ j e. A ( { j } X. C ) " { j } ) ) |
54 |
|
oveq1 |
|- ( m = j -> ( m ( j e. A , k e. C |-> X ) n ) = ( j ( j e. A , k e. C |-> X ) n ) ) |
55 |
53 54
|
mpteq12dv |
|- ( m = j -> ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) = ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) |
56 |
55
|
oveq2d |
|- ( m = j -> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) = ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) ) |
57 |
50 51 56
|
cbvmpt |
|- ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) ) |
58 |
|
vex |
|- j e. _V |
59 |
|
vex |
|- k e. _V |
60 |
58 59
|
elimasn |
|- ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> <. j , k >. e. U_ j e. A ( { j } X. C ) ) |
61 |
|
opeliunxp |
|- ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> ( j e. A /\ k e. C ) ) |
62 |
60 61
|
bitri |
|- ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> ( j e. A /\ k e. C ) ) |
63 |
62
|
baib |
|- ( j e. A -> ( k e. ( U_ j e. A ( { j } X. C ) " { j } ) <-> k e. C ) ) |
64 |
63
|
eqrdv |
|- ( j e. A -> ( U_ j e. A ( { j } X. C ) " { j } ) = C ) |
65 |
64
|
mpteq1d |
|- ( j e. A -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( n e. C |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) |
66 |
|
nfcv |
|- F/_ k j |
67 |
|
nfmpo2 |
|- F/_ k ( j e. A , k e. C |-> X ) |
68 |
|
nfcv |
|- F/_ k n |
69 |
66 67 68
|
nfov |
|- F/_ k ( j ( j e. A , k e. C |-> X ) n ) |
70 |
|
nfcv |
|- F/_ n ( j ( j e. A , k e. C |-> X ) k ) |
71 |
|
oveq2 |
|- ( n = k -> ( j ( j e. A , k e. C |-> X ) n ) = ( j ( j e. A , k e. C |-> X ) k ) ) |
72 |
69 70 71
|
cbvmpt |
|- ( n e. C |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) |
73 |
65 72
|
eqtrdi |
|- ( j e. A -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) ) |
74 |
73
|
adantl |
|- ( ( ph /\ j e. A ) -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) ) |
75 |
|
simprl |
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> j e. A ) |
76 |
|
simprr |
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> k e. C ) |
77 |
35
|
ovmpt4g |
|- ( ( j e. A /\ k e. C /\ X e. B ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) |
78 |
75 76 6 77
|
syl3anc |
|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) |
79 |
78
|
anassrs |
|- ( ( ( ph /\ j e. A ) /\ k e. C ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) |
80 |
79
|
mpteq2dva |
|- ( ( ph /\ j e. A ) -> ( k e. C |-> ( j ( j e. A , k e. C |-> X ) k ) ) = ( k e. C |-> X ) ) |
81 |
74 80
|
eqtrd |
|- ( ( ph /\ j e. A ) -> ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) = ( k e. C |-> X ) ) |
82 |
81
|
oveq2d |
|- ( ( ph /\ j e. A ) -> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) = ( G gsum ( k e. C |-> X ) ) ) |
83 |
82
|
mpteq2dva |
|- ( ph -> ( j e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { j } ) |-> ( j ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) |
84 |
57 83
|
eqtrid |
|- ( ph -> ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) = ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) |
85 |
84
|
oveq2d |
|- ( ph -> ( G gsum ( m e. A |-> ( G gsum ( n e. ( U_ j e. A ( { j } X. C ) " { m } ) |-> ( m ( j e. A , k e. C |-> X ) n ) ) ) ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) ) |
86 |
39 85
|
eqtrd |
|- ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) ) |