Metamath Proof Explorer

Theorem gsumzmhm

Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumzmhm.b 
|- B = ( Base ` G )
gsumzmhm.z 
|- Z = ( Cntz ` G )
gsumzmhm.g 
|- ( ph -> G e. Mnd )
gsumzmhm.h 
|- ( ph -> H e. Mnd )
gsumzmhm.a 
|- ( ph -> A e. V )
gsumzmhm.k 
|- ( ph -> K e. ( G MndHom H ) )
gsumzmhm.f 
|- ( ph -> F : A --> B )
gsumzmhm.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzmhm.0 
|- .0. = ( 0g ` G )
gsumzmhm.w 
|- ( ph -> F finSupp .0. )
Assertion gsumzmhm 
|- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) )

Proof

Step Hyp Ref Expression
1 gsumzmhm.b 
 |-  B = ( Base ` G )
2 gsumzmhm.z 
 |-  Z = ( Cntz ` G )
3 gsumzmhm.g 
 |-  ( ph -> G e. Mnd )
4 gsumzmhm.h 
 |-  ( ph -> H e. Mnd )
5 gsumzmhm.a 
 |-  ( ph -> A e. V )
6 gsumzmhm.k 
 |-  ( ph -> K e. ( G MndHom H ) )
7 gsumzmhm.f 
 |-  ( ph -> F : A --> B )
8 gsumzmhm.c 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
9 gsumzmhm.0 
 |-  .0. = ( 0g ` G )
10 gsumzmhm.w 
 |-  ( ph -> F finSupp .0. )
11 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
12 11 gsumz 
 |-  ( ( H e. Mnd /\ A e. V ) -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( 0g ` H ) )
13 4 5 12 syl2anc 
 |-  ( ph -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( 0g ` H ) )
14 13 adantr 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( 0g ` H ) )
15 9 11 mhm0 
 |-  ( K e. ( G MndHom H ) -> ( K ` .0. ) = ( 0g ` H ) )
16 6 15 syl 
 |-  ( ph -> ( K ` .0. ) = ( 0g ` H ) )
17 16 adantr 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K ` .0. ) = ( 0g ` H ) )
18 14 17 eqtr4d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( K ` .0. ) )
19 1 9 mndidcl 
 |-  ( G e. Mnd -> .0. e. B )
20 3 19 syl 
 |-  ( ph -> .0. e. B )
21 20 ad2antrr 
 |-  ( ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) /\ k e. A ) -> .0. e. B )
22 9 fvexi 
 |-  .0. e. _V
23 22 a1i 
 |-  ( ph -> .0. e. _V )
24 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
25 7 5 24 syl2anc 
 |-  ( ph -> F e. _V )
26 suppimacnv 
 |-  ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
27 25 23 26 syl2anc 
 |-  ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) )
28 ssid 
 |-  ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) )
29 27 28 eqsstrdi 
 |-  ( ph -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) )
30 7 5 23 29 gsumcllem 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> F = ( k e. A |-> .0. ) )
31 eqid 
 |-  ( Base ` H ) = ( Base ` H )
32 1 31 mhmf 
 |-  ( K e. ( G MndHom H ) -> K : B --> ( Base ` H ) )
33 6 32 syl 
 |-  ( ph -> K : B --> ( Base ` H ) )
34 33 feqmptd 
 |-  ( ph -> K = ( x e. B |-> ( K ` x ) ) )
35 34 adantr 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> K = ( x e. B |-> ( K ` x ) ) )
36 fveq2 
 |-  ( x = .0. -> ( K ` x ) = ( K ` .0. ) )
37 21 30 35 36 fmptco 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K o. F ) = ( k e. A |-> ( K ` .0. ) ) )
38 16 mpteq2dv 
 |-  ( ph -> ( k e. A |-> ( K ` .0. ) ) = ( k e. A |-> ( 0g ` H ) ) )
39 38 adantr 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( k e. A |-> ( K ` .0. ) ) = ( k e. A |-> ( 0g ` H ) ) )
40 37 39 eqtrd 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K o. F ) = ( k e. A |-> ( 0g ` H ) ) )
41 40 oveq2d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( K o. F ) ) = ( H gsum ( k e. A |-> ( 0g ` H ) ) ) )
42 30 oveq2d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) )
43 9 gsumz 
 |-  ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
44 3 5 43 syl2anc 
 |-  ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
45 44 adantr 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. )
46 42 45 eqtrd 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum F ) = .0. )
47 46 fveq2d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K ` ( G gsum F ) ) = ( K ` .0. ) )
48 18 41 47 3eqtr4d 
 |-  ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) )
49 48 ex 
 |-  ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) )
50 3 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> G e. Mnd )
51 eqid 
 |-  ( +g ` G ) = ( +g ` G )
52 1 51 mndcl 
 |-  ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
53 52 3expb 
 |-  ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B )
54 50 53 sylan 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B )
55 f1of1 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) )
56 55 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. } ) ) )
57 cnvimass 
 |-  ( `' F " ( _V \ { .0. } ) ) C_ dom F
58 7 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> B )
59 57 58 fssdm 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A )
60 f1ss 
 |-  ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) /\ ( `' F " ( _V \ { .0. } ) ) C_ A ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A )
61 56 59 60 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 )
62 f1f 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A )
63 61 62 syl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A )
64 fco 
 |-  ( ( F : A --> B /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> B )
65 7 63 64 syl2an2r 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> B )
66 65 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. B )
67 simprl 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN )
68 nnuz 
 |-  NN = ( ZZ>= ` 1 )
69 67 68 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. ( ZZ>= ` 1 ) )
70 6 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> K e. ( G MndHom H ) )
71 eqid 
 |-  ( +g ` H ) = ( +g ` H )
72 1 51 71 mhmlin 
 |-  ( ( K e. ( G MndHom H ) /\ x e. B /\ y e. B ) -> ( K ` ( x ( +g ` G ) y ) ) = ( ( K ` x ) ( +g ` H ) ( K ` y ) ) )
73 72 3expb 
 |-  ( ( K e. ( G MndHom H ) /\ ( x e. B /\ y e. B ) ) -> ( K ` ( x ( +g ` G ) y ) ) = ( ( K ` x ) ( +g ` H ) ( K ` y ) ) )
74 70 73 sylan 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( K ` ( x ( +g ` G ) y ) ) = ( ( K ` x ) ( +g ` H ) ( K ` y ) ) )
75 coass 
 |-  ( ( K o. F ) o. f ) = ( K o. ( F o. f ) )
76 75 fveq1i 
 |-  ( ( ( K o. F ) o. f ) ` x ) = ( ( K o. ( F o. f ) ) ` x )
77 fvco3 
 |-  ( ( ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> B /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( ( K o. ( F o. f ) ) ` x ) = ( K ` ( ( F o. f ) ` x ) ) )
78 65 77 sylan 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( ( K o. ( F o. f ) ) ` x ) = ( K ` ( ( F o. f ) ` x ) ) )
79 76 78 syl5req 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( K ` ( ( F o. f ) ` x ) ) = ( ( ( K o. F ) o. f ) ` x ) )
80 54 66 69 74 79 seqhomo 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) = ( seq 1 ( ( +g ` H ) , ( ( K o. F ) o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
81 5 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> A e. V )
82 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 ) )
83 29 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. } ) ) )
84 f1ofo 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) )
85 forn 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
86 84 85 syl 
 |-  ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
87 86 ad2antll 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
88 83 87 sseqtrrd 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ran f )
89 eqid 
 |-  ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. )
90 1 9 51 2 50 81 58 82 67 61 88 89 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. } ) ) ) ) )
91 90 fveq2d 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` ( G gsum F ) ) = ( K ` ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) )
92 eqid 
 |-  ( Cntz ` H ) = ( Cntz ` H )
93 4 adantr 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> H e. Mnd )
94 fco 
 |-  ( ( K : B --> ( Base ` H ) /\ F : A --> B ) -> ( K o. F ) : A --> ( Base ` H ) )
95 33 58 94 syl2an2r 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K o. F ) : A --> ( Base ` H ) )
96 2 92 cntzmhm2 
 |-  ( ( K e. ( G MndHom H ) /\ ran F C_ ( Z ` ran F ) ) -> ( K " ran F ) C_ ( ( Cntz ` H ) ` ( K " ran F ) ) )
97 6 82 96 syl2an2r 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K " ran F ) C_ ( ( Cntz ` H ) ` ( K " ran F ) ) )
98 rnco2 
 |-  ran ( K o. F ) = ( K " ran F )
99 98 fveq2i 
 |-  ( ( Cntz ` H ) ` ran ( K o. F ) ) = ( ( Cntz ` H ) ` ( K " ran F ) )
100 97 98 99 3sstr4g 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran ( K o. F ) C_ ( ( Cntz ` H ) ` ran ( K o. F ) ) )
101 eldifi 
 |-  ( x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) -> x e. A )
102 fvco3 
 |-  ( ( F : A --> B /\ x e. A ) -> ( ( K o. F ) ` x ) = ( K ` ( F ` x ) ) )
103 58 101 102 syl2an 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) ` x ) = ( K ` ( F ` x ) ) )
104 22 a1i 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> .0. e. _V )
105 58 83 81 104 suppssr 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F ` x ) = .0. )
106 105 fveq2d 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` ( F ` x ) ) = ( K ` .0. ) )
107 16 ad2antrr 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` .0. ) = ( 0g ` H ) )
108 103 106 107 3eqtrd 
 |-  ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) ` x ) = ( 0g ` H ) )
109 95 108 suppss 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) supp ( 0g ` H ) ) C_ ( `' F " ( _V \ { .0. } ) ) )
110 109 87 sseqtrrd 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) supp ( 0g ` H ) ) C_ ran f )
111 eqid 
 |-  ( ( ( K o. F ) o. f ) supp ( 0g ` H ) ) = ( ( ( K o. F ) o. f ) supp ( 0g ` H ) )
112 31 11 71 92 93 81 95 100 67 61 110 111 gsumval3 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( H gsum ( K o. F ) ) = ( seq 1 ( ( +g ` H ) , ( ( K o. F ) o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
113 80 91 112 3eqtr4rd 
 |-  ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) )
114 113 expr 
 |-  ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) )
115 114 exlimdv 
 |-  ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) )
116 115 expimpd 
 |-  ( ph -> ( ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) )
117 10 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
118 27 117 eqeltrrd 
 |-  ( ph -> ( `' F " ( _V \ { .0. } ) ) e. Fin )
119 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. } ) ) ) ) )
120 118 119 syl 
 |-  ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) )
121 49 116 120 mpjaod 
 |-  ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) )