Step |
Hyp |
Ref |
Expression |
1 |
|
gsumzcl.b |
|- B = ( Base ` G ) |
2 |
|
gsumzcl.0 |
|- .0. = ( 0g ` G ) |
3 |
|
gsumzcl.z |
|- Z = ( Cntz ` G ) |
4 |
|
gsumzcl.g |
|- ( ph -> G e. Mnd ) |
5 |
|
gsumzcl.a |
|- ( ph -> A e. V ) |
6 |
|
gsumzcl.f |
|- ( ph -> F : A --> B ) |
7 |
|
gsumzcl.c |
|- ( ph -> ran F C_ ( Z ` ran F ) ) |
8 |
|
gsumzcl.w |
|- ( ph -> F finSupp .0. ) |
9 |
|
gsumzf1o.h |
|- ( ph -> H : C -1-1-onto-> A ) |
10 |
2
|
gsumz |
|- ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
11 |
4 5 10
|
syl2anc |
|- ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
12 |
|
f1of1 |
|- ( H : C -1-1-onto-> A -> H : C -1-1-> A ) |
13 |
9 12
|
syl |
|- ( ph -> H : C -1-1-> A ) |
14 |
|
f1dmex |
|- ( ( H : C -1-1-> A /\ A e. V ) -> C e. _V ) |
15 |
13 5 14
|
syl2anc |
|- ( ph -> C e. _V ) |
16 |
2
|
gsumz |
|- ( ( G e. Mnd /\ C e. _V ) -> ( G gsum ( x e. C |-> .0. ) ) = .0. ) |
17 |
4 15 16
|
syl2anc |
|- ( ph -> ( G gsum ( x e. C |-> .0. ) ) = .0. ) |
18 |
11 17
|
eqtr4d |
|- ( ph -> ( G gsum ( k e. A |-> .0. ) ) = ( G gsum ( x e. C |-> .0. ) ) ) |
19 |
18
|
adantr |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( k e. A |-> .0. ) ) = ( G gsum ( x e. C |-> .0. ) ) ) |
20 |
2
|
fvexi |
|- .0. e. _V |
21 |
20
|
a1i |
|- ( ph -> .0. e. _V ) |
22 |
|
ssidd |
|- ( ph -> ( F supp .0. ) C_ ( F supp .0. ) ) |
23 |
6 5 21 22
|
gsumcllem |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> F = ( k e. A |-> .0. ) ) |
24 |
23
|
oveq2d |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) ) |
25 |
|
f1of |
|- ( H : C -1-1-onto-> A -> H : C --> A ) |
26 |
9 25
|
syl |
|- ( ph -> H : C --> A ) |
27 |
26
|
adantr |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> H : C --> A ) |
28 |
27
|
ffvelrnda |
|- ( ( ( ph /\ ( F supp .0. ) = (/) ) /\ x e. C ) -> ( H ` x ) e. A ) |
29 |
27
|
feqmptd |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> H = ( x e. C |-> ( H ` x ) ) ) |
30 |
|
eqidd |
|- ( k = ( H ` x ) -> .0. = .0. ) |
31 |
28 29 23 30
|
fmptco |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> ( F o. H ) = ( x e. C |-> .0. ) ) |
32 |
31
|
oveq2d |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum ( F o. H ) ) = ( G gsum ( x e. C |-> .0. ) ) ) |
33 |
19 24 32
|
3eqtr4d |
|- ( ( ph /\ ( F supp .0. ) = (/) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) |
34 |
33
|
ex |
|- ( ph -> ( ( F supp .0. ) = (/) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) ) |
35 |
9
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> H : C -1-1-onto-> A ) |
36 |
|
f1ococnv2 |
|- ( H : C -1-1-onto-> A -> ( H o. `' H ) = ( _I |` A ) ) |
37 |
35 36
|
syl |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( H o. `' H ) = ( _I |` A ) ) |
38 |
37
|
coeq1d |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = ( ( _I |` A ) o. f ) ) |
39 |
|
f1of1 |
|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) ) |
40 |
39
|
ad2antll |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) ) |
41 |
|
suppssdm |
|- ( F supp .0. ) C_ dom F |
42 |
41 6
|
fssdm |
|- ( ph -> ( F supp .0. ) C_ A ) |
43 |
42
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ A ) |
44 |
|
f1ss |
|- ( ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> ( F supp .0. ) /\ ( F supp .0. ) C_ A ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A ) |
45 |
40 43 44
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A ) |
46 |
|
f1f |
|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A ) |
47 |
|
fcoi2 |
|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) --> A -> ( ( _I |` A ) o. f ) = f ) |
48 |
45 46 47
|
3syl |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( _I |` A ) o. f ) = f ) |
49 |
38 48
|
eqtrd |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( H o. `' H ) o. f ) = f ) |
50 |
|
coass |
|- ( ( H o. `' H ) o. f ) = ( H o. ( `' H o. f ) ) |
51 |
49 50
|
eqtr3di |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> f = ( H o. ( `' H o. f ) ) ) |
52 |
51
|
coeq2d |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) = ( F o. ( H o. ( `' H o. f ) ) ) ) |
53 |
|
coass |
|- ( ( F o. H ) o. ( `' H o. f ) ) = ( F o. ( H o. ( `' H o. f ) ) ) |
54 |
52 53
|
eqtr4di |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. f ) = ( ( F o. H ) o. ( `' H o. f ) ) ) |
55 |
54
|
seqeq3d |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> seq 1 ( ( +g ` G ) , ( F o. f ) ) = seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ) |
56 |
55
|
fveq1d |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) ) |
57 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
58 |
4
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> G e. Mnd ) |
59 |
5
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> A e. V ) |
60 |
6
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> F : A --> B ) |
61 |
7
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran F C_ ( Z ` ran F ) ) |
62 |
|
simprl |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( # ` ( F supp .0. ) ) e. NN ) |
63 |
|
ssid |
|- ( F supp .0. ) C_ ( F supp .0. ) |
64 |
|
f1ofo |
|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) ) |
65 |
|
forn |
|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) ) |
66 |
64 65
|
syl |
|- ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ran f = ( F supp .0. ) ) |
67 |
66
|
ad2antll |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran f = ( F supp .0. ) ) |
68 |
63 67
|
sseqtrrid |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ran f ) |
69 |
|
eqid |
|- ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. ) |
70 |
1 2 57 3 58 59 60 61 62 45 68 69
|
gsumval3 |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( F supp .0. ) ) ) ) |
71 |
15
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> C e. _V ) |
72 |
|
fco |
|- ( ( F : A --> B /\ H : C --> A ) -> ( F o. H ) : C --> B ) |
73 |
6 26 72
|
syl2anc |
|- ( ph -> ( F o. H ) : C --> B ) |
74 |
73
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F o. H ) : C --> B ) |
75 |
|
rncoss |
|- ran ( F o. H ) C_ ran F |
76 |
3
|
cntzidss |
|- ( ( ran F C_ ( Z ` ran F ) /\ ran ( F o. H ) C_ ran F ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) ) |
77 |
7 75 76
|
sylancl |
|- ( ph -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) ) |
78 |
77
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ran ( F o. H ) C_ ( Z ` ran ( F o. H ) ) ) |
79 |
|
f1ocnv |
|- ( H : C -1-1-onto-> A -> `' H : A -1-1-onto-> C ) |
80 |
|
f1of1 |
|- ( `' H : A -1-1-onto-> C -> `' H : A -1-1-> C ) |
81 |
9 79 80
|
3syl |
|- ( ph -> `' H : A -1-1-> C ) |
82 |
81
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> `' H : A -1-1-> C ) |
83 |
|
f1co |
|- ( ( `' H : A -1-1-> C /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> A ) -> ( `' H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> C ) |
84 |
82 45 83
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' H o. f ) : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-> C ) |
85 |
|
ssidd |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( F supp .0. ) C_ ( F supp .0. ) ) |
86 |
6 5
|
fexd |
|- ( ph -> F e. _V ) |
87 |
|
suppimacnv |
|- ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
88 |
86 20 87
|
sylancl |
|- ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
89 |
88
|
eqcomd |
|- ( ph -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) ) |
90 |
89
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) = ( F supp .0. ) ) |
91 |
85 90 67
|
3sstr4d |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ ran f ) |
92 |
|
imass2 |
|- ( ( `' F " ( _V \ { .0. } ) ) C_ ran f -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) ) |
93 |
91 92
|
syl |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' H " ( `' F " ( _V \ { .0. } ) ) ) C_ ( `' H " ran f ) ) |
94 |
|
cnvco |
|- `' ( F o. H ) = ( `' H o. `' F ) |
95 |
94
|
imaeq1i |
|- ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( ( `' H o. `' F ) " ( _V \ { .0. } ) ) |
96 |
|
imaco |
|- ( ( `' H o. `' F ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) ) |
97 |
95 96
|
eqtri |
|- ( `' ( F o. H ) " ( _V \ { .0. } ) ) = ( `' H " ( `' F " ( _V \ { .0. } ) ) ) |
98 |
|
rnco2 |
|- ran ( `' H o. f ) = ( `' H " ran f ) |
99 |
93 97 98
|
3sstr4g |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) |
100 |
|
f1oexrnex |
|- ( ( H : C -1-1-onto-> A /\ A e. V ) -> H e. _V ) |
101 |
9 5 100
|
syl2anc |
|- ( ph -> H e. _V ) |
102 |
|
coexg |
|- ( ( F e. _V /\ H e. _V ) -> ( F o. H ) e. _V ) |
103 |
86 101 102
|
syl2anc |
|- ( ph -> ( F o. H ) e. _V ) |
104 |
|
suppimacnv |
|- ( ( ( F o. H ) e. _V /\ .0. e. _V ) -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) ) |
105 |
103 20 104
|
sylancl |
|- ( ph -> ( ( F o. H ) supp .0. ) = ( `' ( F o. H ) " ( _V \ { .0. } ) ) ) |
106 |
105
|
sseq1d |
|- ( ph -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) ) |
107 |
106
|
adantr |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) <-> ( `' ( F o. H ) " ( _V \ { .0. } ) ) C_ ran ( `' H o. f ) ) ) |
108 |
99 107
|
mpbird |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( ( F o. H ) supp .0. ) C_ ran ( `' H o. f ) ) |
109 |
|
eqid |
|- ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. ) = ( ( ( F o. H ) o. ( `' H o. f ) ) supp .0. ) |
110 |
1 2 57 3 58 71 74 78 62 84 108 109
|
gsumval3 |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum ( F o. H ) ) = ( seq 1 ( ( +g ` G ) , ( ( F o. H ) o. ( `' H o. f ) ) ) ` ( # ` ( F supp .0. ) ) ) ) |
111 |
56 70 110
|
3eqtr4d |
|- ( ( ph /\ ( ( # ` ( F supp .0. ) ) e. NN /\ f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) |
112 |
111
|
expr |
|- ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) ) |
113 |
112
|
exlimdv |
|- ( ( ph /\ ( # ` ( F supp .0. ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) ) |
114 |
113
|
expimpd |
|- ( ph -> ( ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) ) |
115 |
|
fsuppimp |
|- ( F finSupp .0. -> ( Fun F /\ ( F supp .0. ) e. Fin ) ) |
116 |
115
|
simprd |
|- ( F finSupp .0. -> ( F supp .0. ) e. Fin ) |
117 |
|
fz1f1o |
|- ( ( F supp .0. ) e. Fin -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) ) |
118 |
8 116 117
|
3syl |
|- ( ph -> ( ( F supp .0. ) = (/) \/ ( ( # ` ( F supp .0. ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( F supp .0. ) ) ) -1-1-onto-> ( F supp .0. ) ) ) ) |
119 |
34 114 118
|
mpjaod |
|- ( ph -> ( G gsum F ) = ( G gsum ( F o. H ) ) ) |