Metamath Proof Explorer


Theorem gsummhm2

Description: Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsummhm2.b B=BaseG
gsummhm2.z 0˙=0G
gsummhm2.g φGCMnd
gsummhm2.h φHMnd
gsummhm2.a φAV
gsummhm2.k φxBCGMndHomH
gsummhm2.f φkAXB
gsummhm2.w φfinSupp0˙kAX
gsummhm2.1 x=XC=D
gsummhm2.2 x=GkAXC=E
Assertion gsummhm2 φHkAD=E

Proof

Step Hyp Ref Expression
1 gsummhm2.b B=BaseG
2 gsummhm2.z 0˙=0G
3 gsummhm2.g φGCMnd
4 gsummhm2.h φHMnd
5 gsummhm2.a φAV
6 gsummhm2.k φxBCGMndHomH
7 gsummhm2.f φkAXB
8 gsummhm2.w φfinSupp0˙kAX
9 gsummhm2.1 x=XC=D
10 gsummhm2.2 x=GkAXC=E
11 7 fmpttd φkAX:AB
12 1 2 3 4 5 6 11 8 gsummhm φHxBCkAX=xBCGkAX
13 eqidd φkAX=kAX
14 eqidd φxBC=xBC
15 7 13 14 9 fmptco φxBCkAX=kAD
16 15 oveq2d φHxBCkAX=HkAD
17 eqid xBC=xBC
18 1 2 3 5 11 8 gsumcl φGkAXB
19 10 eleq1d x=GkAXCBaseHEBaseH
20 eqid BaseH=BaseH
21 1 20 mhmf xBCGMndHomHxBC:BBaseH
22 6 21 syl φxBC:BBaseH
23 17 fmpt xBCBaseHxBC:BBaseH
24 22 23 sylibr φxBCBaseH
25 19 24 18 rspcdva φEBaseH
26 17 10 18 25 fvmptd3 φxBCGkAX=E
27 12 16 26 3eqtr3d φHkAD=E