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