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 |
|
eqid |
|- ( j e. A , k e. C |-> X ) = ( j e. A , k e. C |-> X ) |
10 |
9
|
mpofun |
|- Fun ( j e. A , k e. C |-> X ) |
11 |
10
|
a1i |
|- ( ph -> Fun ( j e. A , k e. C |-> X ) ) |
12 |
6
|
ralrimivva |
|- ( ph -> A. j e. A A. k e. C X e. B ) |
13 |
9
|
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 ) |
14 |
12 13
|
sylib |
|- ( ph -> ( j e. A , k e. C |-> X ) : U_ j e. A ( { j } X. C ) --> B ) |
15 |
|
nfv |
|- F/ j ph |
16 |
|
nfiu1 |
|- F/_ j U_ j e. A ( { j } X. C ) |
17 |
|
nfcv |
|- F/_ j U |
18 |
16 17
|
nfdif |
|- F/_ j ( U_ j e. A ( { j } X. C ) \ U ) |
19 |
18
|
nfcri |
|- F/ j z e. ( U_ j e. A ( { j } X. C ) \ U ) |
20 |
15 19
|
nfan |
|- F/ j ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) |
21 |
|
nfmpo1 |
|- F/_ j ( j e. A , k e. C |-> X ) |
22 |
|
nfcv |
|- F/_ j z |
23 |
21 22
|
nffv |
|- F/_ j ( ( j e. A , k e. C |-> X ) ` z ) |
24 |
23
|
nfeq1 |
|- F/ j ( ( j e. A , k e. C |-> X ) ` z ) = .0. |
25 |
|
relxp |
|- Rel ( { j } X. C ) |
26 |
25
|
rgenw |
|- A. j e. A Rel ( { j } X. C ) |
27 |
|
reliun |
|- ( Rel U_ j e. A ( { j } X. C ) <-> A. j e. A Rel ( { j } X. C ) ) |
28 |
26 27
|
mpbir |
|- Rel U_ j e. A ( { j } X. C ) |
29 |
|
eldifi |
|- ( z e. ( U_ j e. A ( { j } X. C ) \ U ) -> z e. U_ j e. A ( { j } X. C ) ) |
30 |
29
|
adantl |
|- ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> z e. U_ j e. A ( { j } X. C ) ) |
31 |
|
elrel |
|- ( ( Rel U_ j e. A ( { j } X. C ) /\ z e. U_ j e. A ( { j } X. C ) ) -> E. j E. k z = <. j , k >. ) |
32 |
28 30 31
|
sylancr |
|- ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> E. j E. k z = <. j , k >. ) |
33 |
|
nfv |
|- F/ k ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) |
34 |
|
nfmpo2 |
|- F/_ k ( j e. A , k e. C |-> X ) |
35 |
|
nfcv |
|- F/_ k z |
36 |
34 35
|
nffv |
|- F/_ k ( ( j e. A , k e. C |-> X ) ` z ) |
37 |
36
|
nfeq1 |
|- F/ k ( ( j e. A , k e. C |-> X ) ` z ) = .0. |
38 |
|
simprr |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> z = <. j , k >. ) |
39 |
38
|
fveq2d |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A , k e. C |-> X ) ` z ) = ( ( j e. A , k e. C |-> X ) ` <. j , k >. ) ) |
40 |
|
df-ov |
|- ( j ( j e. A , k e. C |-> X ) k ) = ( ( j e. A , k e. C |-> X ) ` <. j , k >. ) |
41 |
|
simprl |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> z e. ( U_ j e. A ( { j } X. C ) \ U ) ) |
42 |
38 41
|
eqeltrrd |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> <. j , k >. e. ( U_ j e. A ( { j } X. C ) \ U ) ) |
43 |
42
|
eldifad |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> <. j , k >. e. U_ j e. A ( { j } X. C ) ) |
44 |
|
opeliunxp |
|- ( <. j , k >. e. U_ j e. A ( { j } X. C ) <-> ( j e. A /\ k e. C ) ) |
45 |
43 44
|
sylib |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( j e. A /\ k e. C ) ) |
46 |
45
|
simpld |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> j e. A ) |
47 |
45
|
simprd |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> k e. C ) |
48 |
45 6
|
syldan |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> X e. B ) |
49 |
9
|
ovmpt4g |
|- ( ( j e. A /\ k e. C /\ X e. B ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) |
50 |
46 47 48 49
|
syl3anc |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( j ( j e. A , k e. C |-> X ) k ) = X ) |
51 |
40 50
|
eqtr3id |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A , k e. C |-> X ) ` <. j , k >. ) = X ) |
52 |
|
eldifn |
|- ( z e. ( U_ j e. A ( { j } X. C ) \ U ) -> -. z e. U ) |
53 |
52
|
ad2antrl |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> -. z e. U ) |
54 |
38
|
eleq1d |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( z e. U <-> <. j , k >. e. U ) ) |
55 |
|
df-br |
|- ( j U k <-> <. j , k >. e. U ) |
56 |
54 55
|
bitr4di |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( z e. U <-> j U k ) ) |
57 |
53 56
|
mtbid |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> -. j U k ) |
58 |
45 57
|
jca |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A /\ k e. C ) /\ -. j U k ) ) |
59 |
58 8
|
syldan |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> X = .0. ) |
60 |
39 51 59
|
3eqtrd |
|- ( ( ph /\ ( z e. ( U_ j e. A ( { j } X. C ) \ U ) /\ z = <. j , k >. ) ) -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. ) |
61 |
60
|
expr |
|- ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> ( z = <. j , k >. -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. ) ) |
62 |
33 37 61
|
exlimd |
|- ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> ( E. k z = <. j , k >. -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. ) ) |
63 |
20 24 32 62
|
exlimimdd |
|- ( ( ph /\ z e. ( U_ j e. A ( { j } X. C ) \ U ) ) -> ( ( j e. A , k e. C |-> X ) ` z ) = .0. ) |
64 |
14 63
|
suppss |
|- ( ph -> ( ( j e. A , k e. C |-> X ) supp .0. ) C_ U ) |
65 |
7 64
|
ssfid |
|- ( ph -> ( ( j e. A , k e. C |-> X ) supp .0. ) e. Fin ) |
66 |
5
|
ralrimiva |
|- ( ph -> A. j e. A C e. W ) |
67 |
9
|
mpoexxg |
|- ( ( A e. V /\ A. j e. A C e. W ) -> ( j e. A , k e. C |-> X ) e. _V ) |
68 |
4 66 67
|
syl2anc |
|- ( ph -> ( j e. A , k e. C |-> X ) e. _V ) |
69 |
2
|
fvexi |
|- .0. e. _V |
70 |
69
|
a1i |
|- ( ph -> .0. e. _V ) |
71 |
|
isfsupp |
|- ( ( ( j e. A , k e. C |-> X ) e. _V /\ .0. e. _V ) -> ( ( j e. A , k e. C |-> X ) finSupp .0. <-> ( Fun ( j e. A , k e. C |-> X ) /\ ( ( j e. A , k e. C |-> X ) supp .0. ) e. Fin ) ) ) |
72 |
68 70 71
|
syl2anc |
|- ( ph -> ( ( j e. A , k e. C |-> X ) finSupp .0. <-> ( Fun ( j e. A , k e. C |-> X ) /\ ( ( j e. A , k e. C |-> X ) supp .0. ) e. Fin ) ) ) |
73 |
11 65 72
|
mpbir2and |
|- ( ph -> ( j e. A , k e. C |-> X ) finSupp .0. ) |