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 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 ) )