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