Description: Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 6-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsummhm.b | |- B = ( Base ` G ) |
|
gsummhm.z | |- .0. = ( 0g ` G ) |
||
gsummhm.g | |- ( ph -> G e. CMnd ) |
||
gsummhm.h | |- ( ph -> H e. Mnd ) |
||
gsummhm.a | |- ( ph -> A e. V ) |
||
gsummhm.k | |- ( ph -> K e. ( G MndHom H ) ) |
||
gsummhm.f | |- ( ph -> F : A --> B ) |
||
gsummhm.w | |- ( ph -> F finSupp .0. ) |
||
Assertion | gsummhm | |- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsummhm.b | |- B = ( Base ` G ) |
|
2 | gsummhm.z | |- .0. = ( 0g ` G ) |
|
3 | gsummhm.g | |- ( ph -> G e. CMnd ) |
|
4 | gsummhm.h | |- ( ph -> H e. Mnd ) |
|
5 | gsummhm.a | |- ( ph -> A e. V ) |
|
6 | gsummhm.k | |- ( ph -> K e. ( G MndHom H ) ) |
|
7 | gsummhm.f | |- ( ph -> F : A --> B ) |
|
8 | gsummhm.w | |- ( ph -> F finSupp .0. ) |
|
9 | eqid | |- ( Cntz ` G ) = ( Cntz ` G ) |
|
10 | cmnmnd | |- ( G e. CMnd -> G e. Mnd ) |
|
11 | 3 10 | syl | |- ( ph -> G e. Mnd ) |
12 | 1 9 3 7 | cntzcmnf | |- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) ) |
13 | 1 9 11 4 5 6 7 12 2 8 | gsumzmhm | |- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) |