Metamath Proof Explorer

Theorem gsumzoppg

Description: The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumzoppg.b 
|- B = ( Base ` G )
gsumzoppg.0 
|- .0. = ( 0g ` G )
gsumzoppg.z 
|- Z = ( Cntz ` G )
gsumzoppg.o 
|- O = ( oppG ` G )
gsumzoppg.g 
|- ( ph -> G e. Mnd )
gsumzoppg.a 
|- ( ph -> A e. V )
gsumzoppg.f 
|- ( ph -> F : A --> B )
gsumzoppg.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzoppg.n 
|- ( ph -> F finSupp .0. )
Assertion gsumzoppg 
|- ( ph -> ( O gsum F ) = ( G gsum F ) )

Proof

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 7 6 fexd 
 |-  ( ph -> F e. _V )
23 suppimacnv 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
24 22 19 23 sylancl 
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
25 24 sseq1d 
 |-  ( ph -> ( ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) <-> ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) ) )
26 21 25 mpbiri 
 |-  ( ph -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) )
27 7 6 20 26 gsumcllem 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> F = ( k e. A |-> .0. ) )
28 27 oveq2d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( O gsum F ) = ( O gsum ( k e. A |-> .0. ) ) )
29 27 oveq2d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) )
30 18 28 29 3eqtr4d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( O gsum F ) = ( G gsum F ) )
31 30 ex 
 |-  ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) -> ( O gsum F ) = ( G gsum F ) ) )
32 simprl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN )
33 nnuz 
 |-  NN = ( ZZ>= ` 1 )
34 32 33 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. ( ZZ>= ` 1 ) )
35 7 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> B )
36 ffn 
 |-  ( F : A --> B -> F Fn A )
37 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
38 36 37 sylib 
 |-  ( F : A --> B -> F : A -onto-> ran F )
39 fof 
 |-  ( F : A -onto-> ran F -> F : A --> ran F )
40 35 38 39 3syl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> ran F )
41 5 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> G e. Mnd )
42 1 submacs 
 |-  ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` B ) )
43 acsmre 
 |-  ( ( SubMnd ` G ) e. ( ACS ` B ) -> ( SubMnd ` G ) e. ( Moore ` B ) )
44 41 42 43 3syl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( SubMnd ` G ) e. ( Moore ` B ) )
45 eqid 
 |-  ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) )
46 35 frnd 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ B )
47 44 45 46 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 ) )
48 40 47 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 ) )
49 f1of1 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) )
50 49 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. } ) ) )
51 cnvimass 
 |-  ( `' F " ( _V \ { .0. } ) ) C_ dom F
52 51 35 fssdm 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A )
53 f1ss 
 |-  ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) /\ ( `' F " ( _V \ { .0. } ) ) C_ A ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A )
54 50 52 53 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 )
55 f1f 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A )
56 54 55 syl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A )
57 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 ) )
58 48 56 57 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 ) )
59 58 ffvelcdmda 
 |-  ( ( ( 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 ) )
60 45 mrccl 
 |-  ( ( ( SubMnd ` G ) e. ( Moore ` B ) /\ ran F C_ B ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) e. ( SubMnd ` G ) )
61 44 46 60 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 ) )
62 4 oppgsubm 
 |-  ( SubMnd ` G ) = ( SubMnd ` O )
63 61 62 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 ) )
64 eqid 
 |-  ( +g ` O ) = ( +g ` O )
65 64 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 ) )
66 65 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 ) )
67 63 66 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 ) )
68 eqid 
 |-  ( +g ` G ) = ( +g ` G )
69 68 4 64 oppgplus 
 |-  ( x ( +g ` O ) y ) = ( y ( +g ` G ) x )
70 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 ) )
71 eqid 
 |-  ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) = ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) )
72 3 45 71 cntzspan 
 |-  ( ( G e. Mnd /\ ran F C_ ( Z ` ran F ) ) -> ( G |`s ( ( mrCls ` ( SubMnd ` G ) ) ` ran F ) ) e. CMnd )
73 41 70 72 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 )
74 71 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 ) ) ) )
75 61 74 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 ) ) ) )
76 73 75 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 ) ) )
77 76 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 ) ) )
78 68 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 ) )
79 77 78 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 ) )
80 69 79 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 ) )
81 80 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 ) )
82 34 59 67 81 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. } ) ) ) ) )
83 4 1 oppgbas 
 |-  B = ( Base ` O )
84 eqid 
 |-  ( Cntz ` O ) = ( Cntz ` O )
85 41 10 syl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> O e. Mnd )
86 6 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> A e. V )
87 4 3 oppgcntz 
 |-  ( Z ` ran F ) = ( ( Cntz ` O ) ` ran F )
88 70 87 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 ) )
89 suppssdm 
 |-  ( F supp .0. ) C_ dom F
90 24 89 eqsstrrdi 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ dom F )
91 7 90 fssdmd 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ A )
92 91 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A )
93 50 92 53 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 )
94 25 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. } ) ) ) )
95 21 94 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. } ) ) )
96 f1ofo 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) )
97 forn 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
98 96 97 syl 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
99 98 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. } ) ) ) )
100 99 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. } ) ) ) )
101 95 100 mpbird 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ran f )
102 eqid 
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
103 83 12 64 84 85 86 35 88 32 93 101 102 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. } ) ) ) ) )
104 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. } ) ) )
105 104 100 mpbird 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ran f )
106 1 2 68 3 41 86 35 70 32 93 105 102 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. } ) ) ) ) )
107 82 103 106 3eqtr4d 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( O gsum F ) = ( G gsum F ) )
108 107 expr 
 |-  ( ( 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 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 ) ) )
110 109 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 ) ) )
111 9 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
112 24 111 eqeltrrd 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) e. Fin )
113 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. } ) ) ) ) )
114 112 113 syl 
 |-  ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) )
115 31 110 114 mpjaod 
 |-  ( ph -> ( O gsum F ) = ( G gsum F ) )