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 φ G Mnd
gsumzmhm.h φ H Mnd
gsumzmhm.a φ A V
gsumzmhm.k φ K G MndHom H
gsumzmhm.f φ F : A B
gsumzmhm.c φ ran F Z ran F
gsumzmhm.0 0 ˙ = 0 G
gsumzmhm.w φ finSupp 0 ˙ F
Assertion gsumzmhm φ H K F = K G F

Proof

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