Step |
Hyp |
Ref |
Expression |
1 |
|
gsumzoppg.b |
|- B = ( Base ` G ) |
2 |
|
gsumzoppg.0 |
|- .0. = ( 0g ` G ) |
3 |
|
gsumzoppg.z |
|- Z = ( Cntz ` G ) |
4 |
|
gsumzoppg.o |
|- O = ( oppG ` G ) |
5 |
|
gsumzoppg.g |
|- ( ph -> G e. Mnd ) |
6 |
|
gsumzoppg.a |
|- ( ph -> A e. V ) |
7 |
|
gsumzoppg.f |
|- ( ph -> F : A --> B ) |
8 |
|
gsumzoppg.c |
|- ( ph -> ran F C_ ( Z ` ran F ) ) |
9 |
|
gsumzoppg.n |
|- ( ph -> F finSupp .0. ) |
10 |
4
|
oppgmnd |
|- ( G e. Mnd -> O e. Mnd ) |
11 |
5 10
|
syl |
|- ( ph -> O e. Mnd ) |
12 |
4 2
|
oppgid |
|- .0. = ( 0g ` O ) |
13 |
12
|
gsumz |
|- ( ( O e. Mnd /\ A e. V ) -> ( O gsum ( k e. A |-> .0. ) ) = .0. ) |
14 |
11 6 13
|
syl2anc |
|- ( ph -> ( O gsum ( k e. A |-> .0. ) ) = .0. ) |
15 |
2
|
gsumz |
|- ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
16 |
5 6 15
|
syl2anc |
|- ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
17 |
14 16
|
eqtr4d |
|- ( ph -> ( O gsum ( k e. A |-> .0. ) ) = ( G gsum ( k e. A |-> .0. ) ) ) |
18 |
17
|
adantr |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( O gsum ( k e. A |-> .0. ) ) = ( G gsum ( k e. A |-> .0. ) ) ) |
19 |
2
|
fvexi |
|- .0. e. _V |
20 |
19
|
a1i |
|- ( ph -> .0. e. _V ) |
21 |
|
ssid |
|- ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) |
22 |
|
fex |
|- ( ( F : A --> B /\ A e. V ) -> F e. _V ) |
23 |
7 6 22
|
syl2anc |
|- ( ph -> F e. _V ) |
24 |
|
suppimacnv |
|- ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
25 |
23 19 24
|
sylancl |
|- ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
26 |
25
|
sseq1d |
|- ( ph -> ( ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) <-> ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) ) ) |
27 |
21 26
|
mpbiri |
|- ( ph -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) |
28 |
7 6 20 27
|
gsumcllem |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> F = ( k e. A |-> .0. ) ) |
29 |
28
|
oveq2d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( O gsum F ) = ( O gsum ( k e. A |-> .0. ) ) ) |
30 |
28
|
oveq2d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) ) |
31 |
18 29 30
|
3eqtr4d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( O gsum F ) = ( G gsum F ) ) |
32 |
31
|
ex |
|- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) -> ( O gsum F ) = ( G gsum F ) ) ) |
33 |
|
simprl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) |
34 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
35 |
33 34
|
eleqtrdi |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. ( ZZ>= ` 1 ) ) |
36 |
7
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> B ) |
37 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
38 |
|
dffn4 |
|- ( F Fn A <-> F : A -onto-> ran F ) |
39 |
37 38
|
sylib |
|- ( F : A --> B -> F : A -onto-> ran F ) |
40 |
|
fof |
|- ( F : A -onto-> ran F -> F : A --> ran F ) |
41 |
36 39 40
|
3syl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> ran F ) |
42 |
5
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> G e. Mnd ) |
43 |
1
|
submacs |
|- ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` B ) ) |
44 |
|
acsmre |
|- ( ( SubMnd ` G ) e. ( ACS ` B ) -> ( SubMnd ` G ) e. ( Moore ` B ) ) |
45 |
42 43 44
|
3syl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( SubMnd ` G ) e. ( Moore ` B ) ) |
46 |
|
eqid |
|- ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) ) |
47 |
36
|
frnd |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ B ) |
48 |
45 46 47
|
mrcssidd |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
49 |
41 48
|
fssd |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
50 |
|
f1of1 |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) ) |
51 |
50
|
ad2antll |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) ) |
52 |
|
cnvimass |
|- ( `' F " ( _V \ { .0. } ) ) C_ dom F |
53 |
52 36
|
fssdm |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A ) |
54 |
|
f1ss |
|- ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) /\ ( `' F " ( _V \ { .0. } ) ) C_ A ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A ) |
55 |
51 53 54
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A ) |
56 |
|
f1f |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) |
57 |
55 56
|
syl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) |
58 |
|
fco |
|- ( ( F : A --> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
59 |
49 57 58
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
60 |
59
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( ( F o. f ) ` x ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
61 |
46
|
mrccl |
|- ( ( ( SubMnd ` G ) e. ( Moore ` B ) /\ ran F C_ B ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` G ) ) |
62 |
45 47 61
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` G ) ) |
63 |
4
|
oppgsubm |
|- ( SubMnd ` G ) = ( SubMnd ` O ) |
64 |
62 63
|
eleqtrdi |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` O ) ) |
65 |
|
eqid |
|- ( +g ` O ) = ( +g ` O ) |
66 |
65
|
submcl |
|- ( ( ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` O ) /\ x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) -> ( x ( +g ` O ) y ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
67 |
66
|
3expb |
|- ( ( ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` O ) /\ ( x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) -> ( x ( +g ` O ) y ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
68 |
64 67
|
sylan |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ ( x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) -> ( x ( +g ` O ) y ) e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
69 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
70 |
69 4 65
|
oppgplus |
|- ( x ( +g ` O ) y ) = ( y ( +g ` G ) x ) |
71 |
8
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ ( Z ` ran F ) ) |
72 |
|
eqid |
|- ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) = ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) |
73 |
3 46 72
|
cntzspan |
|- ( ( G e. Mnd /\ ran F C_ ( Z ` ran F ) ) -> ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) e. CMnd ) |
74 |
42 71 73
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) e. CMnd ) |
75 |
72 3
|
submcmn2 |
|- ( ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` G ) -> ( ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) e. CMnd <-> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) C_ ( Z ` ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) ) |
76 |
62 75
|
syl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) e. CMnd <-> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) C_ ( Z ` ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) ) |
77 |
74 76
|
mpbid |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) C_ ( Z ` ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) |
78 |
77
|
sselda |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) -> x e. ( Z ` ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) |
79 |
69 3
|
cntzi |
|- ( ( x e. ( Z ` ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) |
80 |
78 79
|
sylan |
|- ( ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) |
81 |
70 80
|
eqtr4id |
|- ( ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) -> ( x ( +g ` O ) y ) = ( x ( +g ` G ) y ) ) |
82 |
81
|
anasss |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ ( x e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) /\ y e. ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) ) -> ( x ( +g ` O ) y ) = ( x ( +g ` G ) y ) ) |
83 |
35 60 68 82
|
seqfeq4 |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( seq 1 ( ( +g ` O ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) |
84 |
4 1
|
oppgbas |
|- B = ( Base ` O ) |
85 |
|
eqid |
|- ( Cntz ` O ) = ( Cntz ` O ) |
86 |
42 10
|
syl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> O e. Mnd ) |
87 |
6
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> A e. V ) |
88 |
4 3
|
oppgcntz |
|- ( Z ` ran F ) = ( ( Cntz ` O ) ` ran F ) |
89 |
71 88
|
sseqtrdi |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ ( ( Cntz ` O ) ` ran F ) ) |
90 |
|
suppssdm |
|- ( F supp .0. ) C_ dom F |
91 |
25 90
|
eqsstrrdi |
|- ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ dom F ) |
92 |
7 91
|
fssdmd |
|- ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ A ) |
93 |
92
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A ) |
94 |
51 93 54
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A ) |
95 |
26
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) <-> ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) ) ) |
96 |
21 95
|
mpbiri |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) |
97 |
|
f1ofo |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) ) |
98 |
|
forn |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) ) |
99 |
97 98
|
syl |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) ) |
100 |
99
|
sseq2d |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) ) |
101 |
100
|
ad2antll |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( F supp .0. ) C_ ran f <-> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) ) |
102 |
96 101
|
mpbird |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ran f ) |
103 |
|
eqid |
|- ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. ) |
104 |
84 12 65 85 86 87 36 89 33 94 102 103
|
gsumval3 |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( O gsum F ) = ( seq 1 ( ( +g ` O ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) |
105 |
27
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) |
106 |
105 101
|
mpbird |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ran f ) |
107 |
1 2 69 3 42 87 36 71 33 94 106 103
|
gsumval3 |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) |
108 |
83 104 107
|
3eqtr4d |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( O gsum F ) = ( G gsum F ) ) |
109 |
108
|
expr |
|- ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( O gsum F ) = ( G gsum F ) ) ) |
110 |
109
|
exlimdv |
|- ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( O gsum F ) = ( G gsum F ) ) ) |
111 |
110
|
expimpd |
|- ( ph -> ( ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) -> ( O gsum F ) = ( G gsum F ) ) ) |
112 |
9
|
fsuppimpd |
|- ( ph -> ( F supp .0. ) e. Fin ) |
113 |
25 112
|
eqeltrrd |
|- ( ph -> ( `' F " ( _V \ { .0. } ) ) e. Fin ) |
114 |
|
fz1f1o |
|- ( ( `' F " ( _V \ { .0. } ) ) e. Fin -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) ) |
115 |
113 114
|
syl |
|- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) ) |
116 |
32 111 115
|
mpjaod |
|- ( ph -> ( O gsum F ) = ( G gsum F ) ) |