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 = ( Base ` G )
gsummhm2.z 
|- .0. = ( 0g ` G )
gsummhm2.g 
|- ( ph -> G e. CMnd )
gsummhm2.h 
|- ( ph -> H e. Mnd )
gsummhm2.a 
|- ( ph -> A e. V )
gsummhm2.k 
|- ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )
gsummhm2.f 
|- ( ( ph /\ k e. A ) -> X e. B )
gsummhm2.w 
|- ( ph -> ( k e. A |-> X ) finSupp .0. )
gsummhm2.1 
|- ( x = X -> C = D )
gsummhm2.2 
|- ( x = ( G gsum ( k e. A |-> X ) ) -> C = E )
Assertion gsummhm2 
|- ( ph -> ( H gsum ( k e. A |-> D ) ) = E )

Proof

Step Hyp Ref Expression
1 gsummhm2.b 
 |-  B = ( Base ` G )
2 gsummhm2.z 
 |-  .0. = ( 0g ` G )
3 gsummhm2.g 
 |-  ( ph -> G e. CMnd )
4 gsummhm2.h 
 |-  ( ph -> H e. Mnd )
5 gsummhm2.a 
 |-  ( ph -> A e. V )
6 gsummhm2.k 
 |-  ( ph -> ( x e. B |-> C ) e. ( G MndHom H ) )
7 gsummhm2.f 
 |-  ( ( ph /\ k e. A ) -> X e. B )
8 gsummhm2.w 
 |-  ( ph -> ( k e. A |-> X ) finSupp .0. )
9 gsummhm2.1 
 |-  ( x = X -> C = D )
10 gsummhm2.2 
 |-  ( x = ( G gsum ( k e. A |-> X ) ) -> C = E )
11 7 fmpttd 
 |-  ( ph -> ( k e. A |-> X ) : A --> B )
12 1 2 3 4 5 6 11 8 gsummhm 
 |-  ( ph -> ( H gsum ( ( x e. B |-> C ) o. ( k e. A |-> X ) ) ) = ( ( x e. B |-> C ) ` ( G gsum ( k e. A |-> X ) ) ) )
13 eqidd 
 |-  ( ph -> ( k e. A |-> X ) = ( k e. A |-> X ) )
14 eqidd 
 |-  ( ph -> ( x e. B |-> C ) = ( x e. B |-> C ) )
15 7 13 14 9 fmptco 
 |-  ( ph -> ( ( x e. B |-> C ) o. ( k e. A |-> X ) ) = ( k e. A |-> D ) )
16 15 oveq2d 
 |-  ( ph -> ( H gsum ( ( x e. B |-> C ) o. ( k e. A |-> X ) ) ) = ( H gsum ( k e. A |-> D ) ) )
17 eqid 
 |-  ( x e. B |-> C ) = ( x e. B |-> C )
18 1 2 3 5 11 8 gsumcl 
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) e. B )
19 10 eleq1d 
 |-  ( x = ( G gsum ( k e. A |-> X ) ) -> ( C e. ( Base ` H ) <-> E e. ( Base ` H ) ) )
20 eqid 
 |-  ( Base ` H ) = ( Base ` H )
21 1 20 mhmf 
 |-  ( ( x e. B |-> C ) e. ( G MndHom H ) -> ( x e. B |-> C ) : B --> ( Base ` H ) )
22 6 21 syl 
 |-  ( ph -> ( x e. B |-> C ) : B --> ( Base ` H ) )
23 17 fmpt 
 |-  ( A. x e. B C e. ( Base ` H ) <-> ( x e. B |-> C ) : B --> ( Base ` H ) )
24 22 23 sylibr 
 |-  ( ph -> A. x e. B C e. ( Base ` H ) )
25 19 24 18 rspcdva 
 |-  ( ph -> E e. ( Base ` H ) )
26 17 10 18 25 fvmptd3 
 |-  ( ph -> ( ( x e. B |-> C ) ` ( G gsum ( k e. A |-> X ) ) ) = E )
27 12 16 26 3eqtr3d 
 |-  ( ph -> ( H gsum ( k e. A |-> D ) ) = E )